changeset 54742 | 7a86358a3c0b |
parent 51717 | 9e7d1c139569 |
child 55380 | 4de48353034e |
--- a/src/CCL/CCL.thy Fri Dec 13 23:53:02 2013 +0100 +++ b/src/CCL/CCL.thy Sat Dec 14 17:28:05 2013 +0100 @@ -280,7 +280,7 @@ fun mk_dstnct_thm rls s = Goal.prove_global thy [] [] (Syntax.read_prop ctxt s) (fn _ => - rewrite_goals_tac defs THEN + rewrite_goals_tac ctxt defs THEN simp_tac (ctxt addsimps (rls @ inj_rls)) 1) in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end