--- a/src/Pure/Syntax/local_syntax.ML Sun Mar 29 19:23:08 2015 +0200
+++ b/src/Pure/Syntax/local_syntax.ML Sun Mar 29 19:24:07 2015 +0200
@@ -55,7 +55,7 @@
val thy_syntax = Sign.syn_of thy;
fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
| update_gram ((false, add, m), decls) =
- Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
+ Syntax.update_const_gram add (Sign.logical_types thy) m decls;
val local_syntax = thy_syntax
|> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));