removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
authorwenzelm
Wed Sep 12 14:46:13 2012 +0200 (2012-09-12)
changeset 493244f28543ae7fa
parent 49323 6dff6b1f5417
child 49332 77c7ce7609cd
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 12 13:56:49 2012 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Sep 12 14:46:13 2012 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4      (binding * string option * mixfix) list ->
     1.5      (Attrib.binding * string) list ->
     1.6      (Facts.ref * Attrib.src list) list ->
     1.7 -    bool -> local_theory -> inductive_result * local_theory
     1.8 +    local_theory -> inductive_result * local_theory
     1.9    val add_inductive_global: inductive_flags ->
    1.10      ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    1.11      thm list -> theory -> inductive_result * theory
    1.12 @@ -81,8 +81,8 @@
    1.13      (binding * string option * mixfix) list ->
    1.14      (binding * string option * mixfix) list ->
    1.15      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
    1.16 -    bool -> local_theory -> inductive_result * local_theory
    1.17 -  val gen_ind_decl: add_ind_def -> bool -> (bool -> local_theory -> local_theory) parser
    1.18 +    local_theory -> inductive_result * local_theory
    1.19 +  val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
    1.20  end;
    1.21  
    1.22  structure Inductive: INDUCTIVE =
    1.23 @@ -1039,7 +1039,7 @@
    1.24      ||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs
    1.25    end;
    1.26  
    1.27 -fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
    1.28 +fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
    1.29    let
    1.30      val ((vars, intrs), _) = lthy
    1.31        |> Proof_Context.set_mode Proof_Context.mode_abbrev
    1.32 @@ -1143,16 +1143,16 @@
    1.33    Scan.optional Parse_Spec.where_alt_specs [] --
    1.34    Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
    1.35    >> (fn (((preds, params), specs), monos) =>
    1.36 -      (snd oo gen_add_inductive mk_def true coind preds params specs monos));
    1.37 +      (snd o gen_add_inductive mk_def true coind preds params specs monos));
    1.38  
    1.39  val ind_decl = gen_ind_decl add_ind_def;
    1.40  
    1.41  val _ =
    1.42 -  Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
    1.43 +  Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
    1.44      (ind_decl false);
    1.45  
    1.46  val _ =
    1.47 -  Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
    1.48 +  Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
    1.49      (ind_decl true);
    1.50  
    1.51  val _ =
     2.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Sep 12 13:56:49 2012 +0200
     2.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Sep 12 14:46:13 2012 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4      (binding * string option * mixfix) list ->
     2.5      (binding * string option * mixfix) list ->
     2.6      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     2.7 -    bool -> local_theory -> Inductive.inductive_result * local_theory
     2.8 +    local_theory -> Inductive.inductive_result * local_theory
     2.9    val mono_add: attribute
    2.10    val mono_del: attribute
    2.11    val codegen_preproc: theory -> thm list -> thm list
    2.12 @@ -574,11 +574,11 @@
    2.13  val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
    2.14  
    2.15  val _ =
    2.16 -  Outer_Syntax.local_theory' @{command_spec "inductive_set"} "define inductive sets"
    2.17 +  Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
    2.18      (ind_set_decl false);
    2.19  
    2.20  val _ =
    2.21 -  Outer_Syntax.local_theory' @{command_spec "coinductive_set"} "define coinductive sets"
    2.22 +  Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
    2.23      (ind_set_decl true);
    2.24  
    2.25  end;