src/HOL/Tools/inductive_realizer.ML

     val ar = length vs + length iTs;
     val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
     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);
 
     val thy1' = thy1 |>
       Theory.copy |>