# HG changeset patch
# User wenzelm
# Date 1010705703 -3600
# Node ID fa4ea2856a31140f082195b6071f1b4962583cc0
# Parent  f7299128cd7d7b3e1e9acc1ca09ee34aacfa8e7e
IsarThy.theorems_i;

diff -r f7299128cd7d -r fa4ea2856a31 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Fri Jan 11 00:34:43 2002 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Jan 11 00:35:03 2002 +0100
@@ -55,9 +55,9 @@
     val read_prop = ProofContext.read_prop (ProofContext.init thy);
     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
     val facts = args |> map (fn ((name, srcs), props) =>
-      (((name, map (Attrib.global_attribute thy) srcs), map (Thm.no_attributes o mk_cases) props),
-        Comment.none));
-  in thy |> IsarThy.have_theorems_i Drule.lemmaK facts end;
+      (((name, map (Attrib.global_attribute thy) srcs),
+        map (Thm.no_attributes o single o mk_cases) props), Comment.none));
+  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
 
 
 (* ind_cases method *)