src/HOL/Tools/datatype_realizer.ML

           ALLGOALS ObjectLogic.atomize_tac,
           rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
             REPEAT (etac allE i) THEN atac i)) 1)]);
 
-    val {path, ...} = Sign.rep_sg sg;
     val ind_name = Thm.name_of_thm induction;
     val vs = map (fn i => List.nth (pnames, i)) is;
     val (thy', thm') = thy
       |> Theory.absolute_path
       |> PureThy.store_thm
         ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
-      |>> Theory.add_path (NameSpace.pack (getOpt (path,[])));
+      |>> Theory.restore_naming thy;
 
     val ivs = Drule.vars_of_terms
       [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
     val rvs = Drule.vars_of_terms [prop_of thm'];
     val ivs1 = map Var (filter_out (fn (_, T) =>

          [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1,
           ALLGOALS (EVERY'
             [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
              resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
 
-    val {path, ...} = Sign.rep_sg sg;
     val exh_name = Thm.name_of_thm exhaustion;
     val (thy', thm') = thy
       |> Theory.absolute_path
       |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
-      |>> Theory.add_path (NameSpace.pack (getOpt (path,[])));
+      |>> Theory.restore_naming thy;
 
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
     val prf = forall_intr_prf (y, forall_intr_prf (P,
       foldr (fn ((p, r), prf) =>
         forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),