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/CTT/rew.ML
changeset 59498 50b60f501b05
parent 58963 26bf09b95dda 
--- a/src/CTT/rew.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/CTT/rew.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -11,7 +11,7 @@
   | peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1));
 
 (*Tactic used for proving conditions for the cond_rls*)
-val prove_cond_tac = eresolve_tac (peEs 5);
+fun prove_cond_tac ctxt = eresolve_tac ctxt (peEs 5);
 
 
 structure TSimp_data: TSIMP_DATA =
@@ -32,11 +32,11 @@
 
 (*Make a rewriting tactic from a normalization tactic*)
 fun make_rew_tac ctxt ntac =
-    TRY (eqintr_tac ctxt)  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  
+    TRY (eqintr_tac ctxt)  THEN  TRYALL (resolve_tac ctxt [TSimp.split_eqn])  THEN  
     ntac;
 
 fun rew_tac ctxt thms = make_rew_tac ctxt
     (TSimp.norm_tac ctxt (standard_congr_rls, thms));
 
 fun hyp_rew_tac ctxt thms = make_rew_tac ctxt
-    (TSimp.cond_norm_tac ctxt (prove_cond_tac, standard_congr_rls, thms));
+    (TSimp.cond_norm_tac ctxt (prove_cond_tac ctxt, standard_congr_rls, thms));
isabelle