--- 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 *)