src/HOL/Tools/datatype_realizer.ML
changeset 18358 0a733e11021a
parent 17959 8db36a108213
child 18929 d81435108688
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Dec 06 06:22:14 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Dec 06 09:04:09 2005 +0100
     1.3 @@ -130,11 +130,11 @@
     1.4  
     1.5      val ind_name = Thm.name_of_thm induction;
     1.6      val vs = map (fn i => List.nth (pnames, i)) is;
     1.7 -    val (thy', thm') = thy
     1.8 +    val (thm', thy') = thy
     1.9        |> Theory.absolute_path
    1.10        |> PureThy.store_thm
    1.11          ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
    1.12 -      |>> Theory.restore_naming thy;
    1.13 +      ||> Theory.restore_naming thy;
    1.14  
    1.15      val ivs = Drule.vars_of_terms
    1.16        [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
    1.17 @@ -200,10 +200,10 @@
    1.18               resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
    1.19  
    1.20      val exh_name = Thm.name_of_thm exhaustion;
    1.21 -    val (thy', thm') = thy
    1.22 +    val (thm', thy') = thy
    1.23        |> Theory.absolute_path
    1.24        |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
    1.25 -      |>> Theory.restore_naming thy;
    1.26 +      ||> Theory.restore_naming thy;
    1.27  
    1.28      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.29      val prf = forall_intr_prf (y, forall_intr_prf (P,