# HG changeset patch
# User nipkow
# Date 1057157877 -7200
# Node ID a9be38579840fc8a414152045b8a90f97a8360ab
# Parent  8dc3e532959a2390ce167d5f04de313952d2210f
Type antiquotations do not use the bracket syntax by default any longer.

diff -r 8dc3e532959a -r a9be38579840 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Tue Jul 01 10:50:26 2003 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Jul 02 16:57:57 2003 +0200
@@ -136,7 +136,7 @@
 fun no_type_brackets () =
   Library.find_first (equal type_bracketsN orf equal no_type_bracketsN)
                      (! print_mode)
-  = Some no_type_bracketsN;
+  <> Some type_bracketsN;
 
 
 (* parse ast translations *)