src/HOL/Tools/inductive_realizer.ML

     val (_, params) = strip_comb S;
     val params' = map dest_Var params;
     val rss = Library.foldl add_rule ([], intrs);
     val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
-    val {path, ...} = Sign.rep_sg (sign_of thy);
+
     val thy1 = thy |>
       Theory.root_path |>
       Theory.add_path (NameSpace.pack prfx);
     val (ty_eqs, rlz_eqs) = split_list
       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);

     val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
       add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
         (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
            elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
 
-  in Theory.add_path (NameSpace.pack (getOpt (path, []))) thy6 end;
+  in Theory.restore_naming thy thy6 end;
 
 fun add_ind_realizers name rsets thy =
   let
     val (_, {intrs, induct, raw_induct, elims, ...}) =
       (case InductivePackage.get_inductive thy name of