diff -r 0ab8750c9342 -r 2551ac44150e src/Pure/Syntax/local_syntax.ML
--- 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)));