src/HOL/Tools/inductive.ML
changeset 49324 4f28543ae7fa
parent 49170 03bee3a6a1b7
child 50214 67fb9a168d10
     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 _ =