src/HOL/Tools/inductive_realizer.ML
changeset 16123 1381e90c2694
parent 15706 bc264e730103
child 16861 7446b4be013b
--- 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