src/ZF/Tools/ind_cases.ML

--- a/src/ZF/Tools/ind_cases.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -55,7 +55,7 @@
     val facts = args |> map (fn ((name, srcs), props) =>
       ((name, map (Attrib.attribute thy) srcs),
         map (Thm.no_attributes o single o mk_cases) props));
-  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
+  in thy |> IsarThy.theorems_i PureThy.lemmaK facts |> snd end;
 
 
 (* ind_cases method *)