--- a/src/CTT/Arith.thy Tue Nov 11 13:44:09 2014 +0100
+++ b/src/CTT/Arith.thy Tue Nov 11 13:50:56 2014 +0100
@@ -174,10 +174,10 @@
local val congr_rls = @{thms congr_rls} in
fun arith_rew_tac ctxt prems = make_rew_tac ctxt
- (Arith_simp.norm_tac ctxt (congr_rls, prems))
+ (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, congr_rls, prems))
end
*}