src/Pure/Isar/instance.ML

     thy
     |> TheoryTarget.instantiation ([tyco], vs, sort)
     |> `(fn ctxt => map (mk_def ctxt) defs)
     |-> (fn defs => fold_map Specification.definition defs)
     |> snd
-    |> LocalTheory.reinit
+    |> LocalTheory.restore
     |> Class.instantiation_instance Class.conclude_instantiation
   else
     thy
     |> Class.instance_arity I (tyco, map snd vs, sort)
   end;