# HG changeset patch
# User wenzelm
# Date 1320009645 -3600
# Node ID adaf2184b79d989dc168f81e46af138b04d4c519
# Parent  5885ec8eb6b0218a619d28045a31efeee377b15d
removed obsolete argument (cf. aa35859c8741);

diff -r 5885ec8eb6b0 -r adaf2184b79d src/Pure/Isar/class.ML
--- 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;
diff -r 5885ec8eb6b0 -r adaf2184b79d src/Pure/Isar/generic_target.ML
--- 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);
diff -r 5885ec8eb6b0 -r adaf2184b79d src/Pure/Isar/named_target.ML
--- 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;
 
 
diff -r 5885ec8eb6b0 -r adaf2184b79d src/Pure/Isar/overloading.ML
--- 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;