Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/typedsimp.ML
changeset 59498 50b60f501b05
parent 59164 ff40c53d1af9 
--- a/src/Provers/typedsimp.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Provers/typedsimp.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -109,16 +109,16 @@
 (*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)
 fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) =
     asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac ctxt  ORELSE'
-    (resolve_tac [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'
+    (resolve_tac ctxt [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'
     subconv_res_tac ctxt congr_rls;
 
 (*Unconditional normalization tactic*)
 fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg)  THEN
-    TRYALL (resolve_tac [red_if_equal]);
+    TRYALL (resolve_tac ctxt [red_if_equal]);
 
 (*Conditional normalization tactic*)
 fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg)  THEN
-    TRYALL (resolve_tac [red_if_equal]);
+    TRYALL (resolve_tac ctxt [red_if_equal]);
 
 end;
 end;
isabelle