# HG changeset patch
# User wenzelm
# Date 1117533194 -7200
# Node ID 1381e90c2694764f2ecf8c4115790f27b1cc3fe7
# Parent  864fda4a40565b4ba58506d20a3a69300999e92a
Theory.restore_naming;

diff -r 864fda4a4056 -r 1381e90c2694 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Tue May 31 11:53:13 2005 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue May 31 11:53:14 2005 +0200
@@ -128,14 +128,13 @@
           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)];
@@ -200,12 +199,11 @@
             [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,
diff -r 864fda4a4056 -r 1381e90c2694 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue May 31 11:53:13 2005 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue May 31 11:53:14 2005 +0200
@@ -287,7 +287,7 @@
     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);
@@ -440,7 +440,7 @@
         (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