# HG changeset patch
# User wenzelm
# Date 1347453973 -7200
# Node ID 4f28543ae7fab0da82484139e9e024fd5b8b71cb
# Parent  6dff6b1f5417a7b4b64e08c47d8f00fc086af885
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);

diff -r 6dff6b1f5417 -r 4f28543ae7fa src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Sep 12 13:56:49 2012 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Sep 12 14:46:13 2012 +0200
@@ -49,7 +49,7 @@
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list ->
     (Facts.ref * Attrib.src list) list ->
-    bool -> local_theory -> inductive_result * local_theory
+    local_theory -> inductive_result * local_theory
   val add_inductive_global: inductive_flags ->
     ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
     thm list -> theory -> inductive_result * theory
@@ -81,8 +81,8 @@
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
-    bool -> local_theory -> inductive_result * local_theory
-  val gen_ind_decl: add_ind_def -> bool -> (bool -> local_theory -> local_theory) parser
+    local_theory -> inductive_result * local_theory
+  val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
 end;
 
 structure Inductive: INDUCTIVE =
@@ -1039,7 +1039,7 @@
     ||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs
   end;
 
-fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
+fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
   let
     val ((vars, intrs), _) = lthy
       |> Proof_Context.set_mode Proof_Context.mode_abbrev
@@ -1143,16 +1143,16 @@
   Scan.optional Parse_Spec.where_alt_specs [] --
   Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
   >> (fn (((preds, params), specs), monos) =>
-      (snd oo gen_add_inductive mk_def true coind preds params specs monos));
+      (snd o gen_add_inductive mk_def true coind preds params specs monos));
 
 val ind_decl = gen_ind_decl add_ind_def;
 
 val _ =
-  Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
+  Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
     (ind_decl false);
 
 val _ =
-  Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
+  Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
     (ind_decl true);
 
 val _ =
diff -r 6dff6b1f5417 -r 4f28543ae7fa src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Sep 12 13:56:49 2012 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Sep 12 14:46:13 2012 +0200
@@ -21,7 +21,7 @@
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
-    bool -> local_theory -> Inductive.inductive_result * local_theory
+    local_theory -> Inductive.inductive_result * local_theory
   val mono_add: attribute
   val mono_del: attribute
   val codegen_preproc: theory -> thm list -> thm list
@@ -574,11 +574,11 @@
 val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
 
 val _ =
-  Outer_Syntax.local_theory' @{command_spec "inductive_set"} "define inductive sets"
+  Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
     (ind_set_decl false);
 
 val _ =
-  Outer_Syntax.local_theory' @{command_spec "coinductive_set"} "define coinductive sets"
+  Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
     (ind_set_decl true);
 
 end;