src/CTT/Arith.thy
changeset 59498 50b60f501b05
parent 58977 9576b510f6a2
child 60770 240563fbf41d
--- a/src/CTT/Arith.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/CTT/Arith.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -177,7 +177,7 @@
   (Arith_simp.norm_tac ctxt (congr_rls, prems))
 
 fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt
-  (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems))
+  (Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, congr_rls, prems))
 
 end
 *}