diff -r 9c19e15c8548 -r 6d6839a948cf src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Mon Jun 03 23:58:20 2019 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Jun 04 13:08:05 2019 +0200
@@ -262,7 +262,7 @@
           handle ERROR msg => cat_error msg "Failed to prove definitional specification";
       in
         def_thm
-        |> singleton (Variable.export def_ctxt def_ctxt0)
+        |> singleton (Proof_Context.export def_ctxt def_ctxt0)
         |> Drule.zero_var_indexes
       end;
   in (((c, T), rhs), prove) end;