diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/Isar/generic_target.ML
--- 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;