# HG changeset patch
# User berghofe
# Date 1190968251 -7200
# Node ID d0e7a4672c6d392a1a39c2631475deaa9de51de3
# Parent  dcb8cf5fc99cba8ffd8a9660745a09098f522339
add_inductive_i now takes typ instead of typ option as argument.

diff -r dcb8cf5fc99c -r d0e7a4672c6d src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Fri Sep 28 10:29:35 2007 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Fri Sep 28 10:30:51 2007 +0200
@@ -12,8 +12,8 @@
   val to_pred_att: thm list -> attribute
   val pred_set_conv_att: attribute
   val add_inductive_i: bool -> bstring -> bool -> bool -> bool ->
-    (string * typ option * mixfix) list ->
-    (string * typ option) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
+    ((string * typ) * mixfix) list ->
+    (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
       local_theory -> InductivePackage.inductive_result * local_theory
   val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
     (string * string option * mixfix) list ->