Permalink
Browse files

fix ml_monadScript.sml for latest HOL

This was required for it to build on my machine with HOL 3aa000c.
Feel free to replace with an equivalent fix.
  • Loading branch information...
xrchz committed Mar 5, 2013
1 parent 521f9d1 commit 0d4d370ac8aa7e7dcbab651dc6a083f1c6116396
Showing with 1 addition and 1 deletion.
  1. +1 −1 hol-light/ml_monadScript.sml
@@ -341,7 +341,7 @@ val EvalM_Var_SIMP = store_thm("EvalM_Var_SIMP",
\\ ASM_SIMP_TAC (srw_ss()) [Once evaluate'_cases]);
val option_CASE_LEMMA2 = prove(
- ``!topt. (case topt of NONE => v | SOME (t,y) => v) = v``,
+ Pmatch.with_classic_heuristic Term `!topt. (case topt of NONE => v | SOME z => v) = v`,
Cases \\ SRW_TAC [] [] \\ Cases_on `x` \\ SRW_TAC [] []);
val EvalM_Recclosure = store_thm("EvalM_Recclosure",

0 comments on commit 0d4d370

Please sign in to comment.