src/Pure/Isar/instance.ML

     thy
     |> TheoryTarget.instantiation arities
     |> `(fn ctxt => map (mk_def ctxt) defs)
     |-> (fn defs => fold_map Specification.definition defs)
     |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
-    ||> LocalTheory.exit
-    ||> ProofContext.theory_of
-    ||> TheoryTarget.instantiation arities
+    ||> LocalTheory.reinit
+    (*||> ProofContext.theory_of
+    ||> TheoryTarget.instantiation arities*)
     |-> (fn defs => do_proof defs)
   else
     thy
     |> do_proof' arities
   end;