src/HOL/Tools/inductive_package.ML
changeset 12128 25565bbbd246
parent 12109 bd6eb9194a5d
child 12165 14e94ad99861
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Nov 09 22:50:32 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 09 22:50:58 2001 +0100
     1.3 @@ -858,9 +858,9 @@
     1.4      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
     1.5      val (cs', intr_ts') = unify_consts sign cs intr_ts;
     1.6  
     1.7 -    val ((thy', con_defs), monos) = thy
     1.8 +    val (thy', (monos, con_defs)) = thy
     1.9        |> IsarThy.apply_theorems raw_monos
    1.10 -      |> apfst (IsarThy.apply_theorems raw_con_defs);
    1.11 +      |>>> IsarThy.apply_theorems raw_con_defs;
    1.12    in
    1.13      add_inductive_i verbose false "" coind false false cs'
    1.14        ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'