removed obsolete argument (cf. aa35859c8741);
--- a/src/Pure/Isar/class.ML Sun Oct 30 09:42:13 2011 +0100
+++ b/src/Pure/Isar/class.ML Sun Oct 30 22:20:45 2011 +0100
@@ -560,7 +560,7 @@
abbrev = Generic_Target.abbrev
(fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
Generic_Target.theory_abbrev prmode ((b, mx), t)),
- declaration = Generic_Target.theory_declaration o #syntax,
+ declaration = K Generic_Target.theory_declaration,
pretty = pretty,
exit = Local_Theory.target_of o conclude}
end;
--- a/src/Pure/Isar/generic_target.ML Sun Oct 30 09:42:13 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML Sun Oct 30 22:20:45 2011 +0100
@@ -20,7 +20,7 @@
string * bool -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val theory_declaration: bool -> declaration -> local_theory -> local_theory
+ val theory_declaration: declaration -> local_theory -> local_theory
val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
@@ -185,7 +185,7 @@
(** primitive theory operations **)
-fun theory_declaration syntax decl lthy =
+fun theory_declaration decl lthy =
let
val global_decl = Morphism.form
(Morphism.transform (Local_Theory.global_morphism lthy) decl);
--- a/src/Pure/Isar/named_target.ML Sun Oct 30 09:42:13 2011 +0100
+++ b/src/Pure/Isar/named_target.ML Sun Oct 30 22:20:45 2011 +0100
@@ -52,12 +52,12 @@
val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
in
lthy
- |> pervasive ? Generic_Target.theory_declaration syntax decl
+ |> pervasive ? Generic_Target.theory_declaration decl
|> Local_Theory.target (add locale locale_decl)
end;
fun target_declaration (Target {target, ...}) params =
- if target = "" then Generic_Target.theory_declaration (#syntax params)
+ if target = "" then Generic_Target.theory_declaration
else locale_declaration target params;
--- a/src/Pure/Isar/overloading.ML Sun Oct 30 09:42:13 2011 +0100
+++ b/src/Pure/Isar/overloading.ML Sun Oct 30 22:20:45 2011 +0100
@@ -206,7 +206,7 @@
abbrev = Generic_Target.abbrev
(fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
Generic_Target.theory_abbrev prmode ((b, mx), t)),
- declaration = Generic_Target.theory_declaration o #syntax,
+ declaration = K Generic_Target.theory_declaration,
pretty = pretty,
exit = Local_Theory.target_of o conclude}
end;