# HG changeset patch
# User wenzelm
# Date 1160353209 -7200
# Node ID ee6e3597bb4d62632c07e17974bb2e6b707aea80
# Parent  dcb0a3e2f1bd3485913ba3a1edcee1d09bb3e79a
PureThy.note_thmss_i;

diff -r dcb0a3e2f1bd -r ee6e3597bb4d src/ZF/Tools/ind_cases.ML
--- 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 *)