src/Pure/Isar/generic_target.ML

--- a/src/Pure/Isar/generic_target.ML	Thu Sep 24 13:33:42 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Sep 24 23:33:29 2015 +0200
@@ -162,7 +162,7 @@
 
     val ((_, def), lthy3) = lthy2
       |> Local_Theory.background_theory_result
-        (Thm.add_def lthy2 false false
+        (Thm.add_def (Proof_Context.defs_context lthy2) false false
           (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;