adapted args of IsarThy.have_theorems_i;
authorwenzelm
Thu, 29 Jun 2000 22:38:30 +0200
changeset 9201 435fef035d7f
parent 9200 3a44c828be1d
child 9202 738056d60a2a
adapted args of IsarThy.have_theorems_i;
src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Jun 29 22:37:24 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jun 29 22:38:30 2000 +0200
@@ -506,7 +506,7 @@
             (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
         in
           thy |> IsarThy.have_theorems_i
-            (((name, atts), map Thm.no_attributes thms), comment)
+            [(((name, atts), map Thm.no_attributes thms), comment)]
         end)
   end;