# HG changeset patch
# User wenzelm
# Date 1010705323 -3600
# Node ID e29800eba5d10e350eba8052dac53f88b77e2c23
# Parent  31672377dadcb2d5959f9a4f6449a5730194f5db
IsarThy.theorems_i;

diff -r 31672377dadc -r e29800eba5d1 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Jan 11 00:28:24 2002 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Jan 11 00:28:43 2002 +0100
@@ -587,9 +587,9 @@
     val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
     val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
 
-    val facts = args |> map (fn (((name, atts), props), comment) =>
-      (((name, map (prep_att thy) atts), map (Thm.no_attributes o mk_cases) props), comment));
-  in thy |> IsarThy.have_theorems_i Drule.lemmaK facts end;
+    val facts = args |> map (fn (((a, atts), props), comment) =>
+     (((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props), comment));
+  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
 
 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;