# HG changeset patch
# User berghofe
# Date 908985158 -7200
# Node ID e5094d678285aead94ad5efb92cac959bf5764c6
# Parent  0d28dbe484b6717a1fc33e90d8e807e6631432f9
Changed interface of add_inductive: monos and con_defs are now
lists of xstrings.

diff -r 0d28dbe484b6 -r e5094d678285 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Oct 21 17:48:02 1998 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Oct 21 17:52:38 1998 +0200
@@ -37,7 +37,7 @@
        mk_cases:thm list -> string -> thm, mono:thm,
        unfold:thm}
   val add_inductive : bool -> bool -> string list -> string list
-    -> thm list -> thm list -> theory -> theory *
+    -> xstring list -> xstring list -> theory -> theory *
       {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
        intrs:thm list,
        mk_cases:thm list -> string -> thm, mono:thm,
@@ -600,7 +600,8 @@
     val intr_ts'' = map subst intr_ts';
 
   in add_inductive_i verbose false "" coind false false cs'' intr_ts''
-    monos con_defs thy
+    (map (Attribute.thm_of) (PureThy.get_tthmss thy monos))
+    (map (Attribute.thm_of) (PureThy.get_tthmss thy con_defs)) thy
   end;
 
 end;