src/HOL/Tools/inductive_realizer.ML
changeset 21858 05f57309170c
parent 21646 c07b5b0e8492
child 22271 51a80e238b29
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -296,12 +296,12 @@
     val (_, params) = strip_comb S;
     val params' = map dest_Var params;
     val rss = [] |> fold add_rule intrs;
-    val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
+    val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
 
     val thy1 = thy |>
       Theory.root_path |>
-      Theory.add_path (NameSpace.pack prfx);
+      Theory.add_path (NameSpace.implode prfx);
     val (ty_eqs, rlz_eqs) = split_list
       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);