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