src/HOL/Tools/inductive_package.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18463 56414918dbbd
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -583,7 +583,7 @@
     1.4  
     1.5      val facts = args |> map (fn ((a, atts), props) =>
     1.6       ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
     1.7 -  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
     1.8 +  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
     1.9  
    1.10  val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
    1.11  val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
    1.12 @@ -864,7 +864,7 @@
    1.13      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
    1.14      val (cs', intr_ts') = unify_consts thy cs intr_ts;
    1.15  
    1.16 -    val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
    1.17 +    val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos;
    1.18    in
    1.19      add_inductive_i verbose false "" coind false false cs'
    1.20        ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'