src/ZF/Tools/inductive_package.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18643 89a7978f90e1
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -567,16 +567,16 @@
     1.4      val dom_sum = read Ind_Syntax.iT sdom_sum;
     1.5      val intr_tms = map (read propT o snd o fst) sintrs;
     1.6      val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs;
     1.7 -
     1.8 -    val (thy', (((monos, con_defs), type_intrs), type_elims)) = thy
     1.9 -      |> IsarThy.apply_theorems raw_monos
    1.10 -      |>>> IsarThy.apply_theorems raw_con_defs
    1.11 -      |>>> IsarThy.apply_theorems raw_type_intrs
    1.12 -      |>>> IsarThy.apply_theorems raw_type_elims;
    1.13    in
    1.14 -    add_inductive_i true (rec_tms, dom_sum) intr_specs
    1.15 -      (monos, con_defs, type_intrs, type_elims) thy'
    1.16 -  end
    1.17 +    thy
    1.18 +    |> IsarThy.apply_theorems raw_monos
    1.19 +    ||>> IsarThy.apply_theorems raw_con_defs
    1.20 +    ||>> IsarThy.apply_theorems raw_type_intrs
    1.21 +    ||>> IsarThy.apply_theorems raw_type_elims
    1.22 +    |-> (fn (((monos, con_defs), type_intrs), type_elims) =>
    1.23 +          add_inductive_i true (rec_tms, dom_sum) intr_specs
    1.24 +            (monos, con_defs, type_intrs, type_elims))
    1.25 +  end;
    1.26  
    1.27  
    1.28  (* outer syntax *)