PureThy.note_thmss_i;

--- a/src/ZF/Tools/ind_cases.ML	Mon Oct 09 02:20:08 2006 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Mon Oct 09 02:20:09 2006 +0200
@@ -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 PureThy.lemmaK facts |> snd end;
+  in thy |> PureThy.note_thmss_i "" facts |> snd end;
 
 
 (* ind_cases method *)