IsarThy.theorems_i;
authorwenzelm
Fri Jan 11 00:28:43 2002 +0100 (2002-01-11 ago)
changeset 12709e29800eba5d1
parent 12708 31672377dadc
child 12710 d9e0674653b3
IsarThy.theorems_i;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jan 11 00:28:24 2002 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jan 11 00:28:43 2002 +0100
     1.3 @@ -587,9 +587,9 @@
     1.4      val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
     1.5      val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
     1.6  
     1.7 -    val facts = args |> map (fn (((name, atts), props), comment) =>
     1.8 -      (((name, map (prep_att thy) atts), map (Thm.no_attributes o mk_cases) props), comment));
     1.9 -  in thy |> IsarThy.have_theorems_i Drule.lemmaK facts end;
    1.10 +    val facts = args |> map (fn (((a, atts), props), comment) =>
    1.11 +     (((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props), comment));
    1.12 +  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
    1.13  
    1.14  val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
    1.15  val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;