--- a/src/Pure/Isar/generic_target.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/generic_target.ML Sun Mar 01 23:35:41 2015 +0100
@@ -206,8 +206,7 @@
(*result*)
val def =
Thm.transitive local_def global_def
- |> Local_Defs.contract lthy3 defs
- (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
+ |> Local_Defs.contract lthy3 defs (Proof_Context.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));
val ([(res_name, [res])], lthy4) = lthy3
|> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
in ((lhs, (res_name, res)), lthy4) end;