removed obsolete argument (cf. aa35859c8741);
authorwenzelm
Sun Oct 30 22:20:45 2011 +0100 (2011-10-30 ago)
changeset 45310adaf2184b79d
parent 45309 5885ec8eb6b0
child 45311 ca9e66c523a2
removed obsolete argument (cf. aa35859c8741);
src/Pure/Isar/class.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/overloading.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sun Oct 30 09:42:13 2011 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sun Oct 30 22:20:45 2011 +0100
     1.3 @@ -560,7 +560,7 @@
     1.4          abbrev = Generic_Target.abbrev
     1.5            (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
     1.6              Generic_Target.theory_abbrev prmode ((b, mx), t)),
     1.7 -        declaration = Generic_Target.theory_declaration o #syntax,
     1.8 +        declaration = K Generic_Target.theory_declaration,
     1.9          pretty = pretty,
    1.10          exit = Local_Theory.target_of o conclude}
    1.11    end;
     2.1 --- a/src/Pure/Isar/generic_target.ML	Sun Oct 30 09:42:13 2011 +0100
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Oct 30 22:20:45 2011 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4      string * bool -> (binding * mixfix) * term -> local_theory ->
     2.5      (term * term) * local_theory
     2.6  
     2.7 -  val theory_declaration: bool -> declaration -> local_theory -> local_theory
     2.8 +  val theory_declaration: declaration -> local_theory -> local_theory
     2.9    val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
    2.10      term list * term list -> local_theory -> (term * thm) * local_theory
    2.11    val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
    2.12 @@ -185,7 +185,7 @@
    2.13  
    2.14  (** primitive theory operations **)
    2.15  
    2.16 -fun theory_declaration syntax decl lthy =
    2.17 +fun theory_declaration decl lthy =
    2.18    let
    2.19      val global_decl = Morphism.form
    2.20        (Morphism.transform (Local_Theory.global_morphism lthy) decl);
     3.1 --- a/src/Pure/Isar/named_target.ML	Sun Oct 30 09:42:13 2011 +0100
     3.2 +++ b/src/Pure/Isar/named_target.ML	Sun Oct 30 22:20:45 2011 +0100
     3.3 @@ -52,12 +52,12 @@
     3.4      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
     3.5    in
     3.6      lthy
     3.7 -    |> pervasive ? Generic_Target.theory_declaration syntax decl
     3.8 +    |> pervasive ? Generic_Target.theory_declaration decl
     3.9      |> Local_Theory.target (add locale locale_decl)
    3.10    end;
    3.11  
    3.12  fun target_declaration (Target {target, ...}) params =
    3.13 -  if target = "" then Generic_Target.theory_declaration (#syntax params)
    3.14 +  if target = "" then Generic_Target.theory_declaration
    3.15    else locale_declaration target params;
    3.16  
    3.17  
     4.1 --- a/src/Pure/Isar/overloading.ML	Sun Oct 30 09:42:13 2011 +0100
     4.2 +++ b/src/Pure/Isar/overloading.ML	Sun Oct 30 22:20:45 2011 +0100
     4.3 @@ -206,7 +206,7 @@
     4.4          abbrev = Generic_Target.abbrev
     4.5            (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
     4.6              Generic_Target.theory_abbrev prmode ((b, mx), t)),
     4.7 -        declaration = Generic_Target.theory_declaration o #syntax,
     4.8 +        declaration = K Generic_Target.theory_declaration,
     4.9          pretty = pretty,
    4.10          exit = Local_Theory.target_of o conclude}
    4.11    end;