compactified

--- a/src/Pure/Isar/generic_target.ML	Thu May 22 15:49:36 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu May 22 16:59:49 2014 +0200
@@ -25,10 +25,10 @@
     string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
   val background_declaration: declaration -> local_theory -> local_theory
   val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
-  val standard_declaration: (int -> int -> bool) -> declaration -> local_theory -> local_theory
+  val standard_declaration: (int * int -> bool) -> declaration -> local_theory -> local_theory
   val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term ->
     Context.generic -> Context.generic
-  val const_declaration: (int -> int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
+  val const_declaration: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
   val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
@@ -231,7 +231,7 @@
 
 fun standard_declaration pred decl lthy =
   Local_Theory.map_contexts (fn level => fn ctxt =>
-    if pred (Local_Theory.level lthy) level
+    if pred (Local_Theory.level lthy, level)
     then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
     else ctxt) lthy;
 
@@ -308,8 +308,7 @@
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) =>
-        const_declaration (fn this_level => fn level => level <> this_level)
-          Syntax.mode_default ((b, mx), lhs)
+        const_declaration (op <>) Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def));
 
 fun theory_notes kind global_facts local_facts =
@@ -326,10 +325,10 @@
       (fn (lhs, _) =>  (* FIXME type_params!? *)
         Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs))
   #-> (fn lhs =>
-        const_declaration (fn this_level => fn level => level <> this_level) prmode
+        const_declaration (op <>) prmode
           ((b, if null xs then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
 fun theory_declaration decl =
-  background_declaration decl #> standard_declaration ((K o K) true) decl;
+  background_declaration decl #> standard_declaration (K true) decl;
 
 end;

--- a/src/Pure/Isar/named_target.ML	Thu May 22 15:49:36 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu May 22 16:59:49 2014 +0200
@@ -78,7 +78,7 @@
       not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
     end) #>
   Generic_Target.const_declaration
-    (fn this_level => fn level => level <> 0 andalso level <> this_level) prmode ((b, mx), rhs);
+    (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
 
 
 (* define *)
@@ -131,7 +131,7 @@
     lthy
     |> pervasive ? Generic_Target.background_declaration decl
     |> Generic_Target.locale_declaration target syntax decl
-    |> Generic_Target.standard_declaration (fn _ => fn level => level <> 0) decl;
+    |> Generic_Target.standard_declaration (fn (_, other) => other <> 0) decl;
 
 
 (* subscription *)