add_inductive_i now takes typ instead of typ option as argument.
--- 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 ->