src/HOL/Tools/datatype_realizer.ML
changeset 26481 92e901171cc8
parent 26359 6d437bde2f1d
child 26626 c6231d64d264
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sat Mar 29 19:14:00 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Mar 29 19:14:03 2008 +0100
     1.3 @@ -131,8 +131,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
     1.8 -        ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
     1.9 +      |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm)
    1.10        ||> Sign.restore_naming thy;
    1.11  
    1.12      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
    1.13 @@ -198,7 +197,7 @@
    1.14      val exh_name = Thm.get_name exhaustion;
    1.15      val (thm', thy') = thy
    1.16        |> Sign.absolute_path
    1.17 -      |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
    1.18 +      |> PureThy.store_thm (exh_name ^ "_P_correctness", thm)
    1.19        ||> Sign.restore_naming thy;
    1.20  
    1.21      val P = Var (("P", 0), rT' --> HOLogic.boolT);