--- a/src/Pure/Syntax/type_ext.ML Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Syntax/type_ext.ML Tue Mar 21 12:18:15 2006 +0100
@@ -140,14 +140,14 @@
val no_bracketsN = "no_brackets";
fun no_brackets () =
- find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)
+ find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (! print_mode)
= SOME no_bracketsN;
val type_bracketsN = "type_brackets";
val no_type_bracketsN = "no_type_brackets";
fun no_type_brackets () =
- Library.find_first (equal type_bracketsN orf equal no_type_bracketsN) (! print_mode)
+ find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (! print_mode)
<> SOME type_bracketsN;