src/HOL/Tools/datatype_realizer.ML
changeset 30435 e62d6ecab6ad
parent 30364 577edc39b501
child 31458 b1cf26f2919b
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Mar 11 15:38:25 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Mar 11 15:42:19 2009 +0100
     1.3 @@ -128,8 +128,9 @@
     1.4      val ind_name = Thm.get_name induction;
     1.5      val vs = map (fn i => List.nth (pnames, i)) is;
     1.6      val (thm', thy') = thy
     1.7 -      |> Sign.absolute_path
     1.8 -      |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
     1.9 +      |> Sign.root_path
    1.10 +      |> PureThy.store_thm
    1.11 +        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
    1.12        ||> Sign.restore_naming thy;
    1.13  
    1.14      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
    1.15 @@ -194,8 +195,8 @@
    1.16  
    1.17      val exh_name = Thm.get_name exhaustion;
    1.18      val (thm', thy') = thy
    1.19 -      |> Sign.absolute_path
    1.20 -      |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm)
    1.21 +      |> Sign.root_path
    1.22 +      |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
    1.23        ||> Sign.restore_naming thy;
    1.24  
    1.25      val P = Var (("P", 0), rT' --> HOLogic.boolT);