add_inductive_i now takes typ instead of typ option as argument.
authorberghofe
Fri, 28 Sep 2007 10:30:51 +0200
changeset 24745 d0e7a4672c6d
parent 24744 dcb8cf5fc99c
child 24746 6d42be359d57
add_inductive_i now takes typ instead of typ option as argument.
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 ->