src/Pure/Isar/named_target.ML

         orelse same_shape);
     in
       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 *)
 
 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params =

   if target = "" then Generic_Target.theory_declaration decl lthy
   else
     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 *)
 
 fun target_subscription (Target {target, ...}) =