src/HOL/Tools/datatype_realizer.ML
changeset 29579 cb520b766e00
parent 28814 463c9e9111ae
child 30190 479806475f3c
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Jan 21 16:47:03 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Jan 21 16:47:04 2009 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4      val vs = map (fn i => List.nth (pnames, i)) is;
     1.5      val (thm', thy') = thy
     1.6        |> Sign.absolute_path
     1.7 -      |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm)
     1.8 +      |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
     1.9        ||> Sign.restore_naming thy;
    1.10  
    1.11      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
    1.12 @@ -196,7 +196,7 @@
    1.13      val exh_name = Thm.get_name exhaustion;
    1.14      val (thm', thy') = thy
    1.15        |> Sign.absolute_path
    1.16 -      |> PureThy.store_thm (exh_name ^ "_P_correctness", thm)
    1.17 +      |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm)
    1.18        ||> Sign.restore_naming thy;
    1.19  
    1.20      val P = Var (("P", 0), rT' --> HOLogic.boolT);