src/HOL/Tools/inductive_package.ML
changeset 18799 f137c5e971f5
parent 18787 5784fe1b5657
child 18921 f47c46d7d654
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jan 27 18:29:33 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jan 27 19:03:02 2006 +0100
     1.3 @@ -570,7 +570,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 |> snd end;
     1.8 +  in thy |> IsarThy.theorems_i PureThy.lemmaK facts |> snd end;
     1.9  
    1.10  val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
    1.11  val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;