src/Pure/Syntax/syn_ext.ML
changeset 1145 d25b863ab2ac
parent 922 196ca0973a6d
child 1178 b28c6ecc3e6d
--- a/src/Pure/Syntax/syn_ext.ML	Tue Jun 06 10:40:01 1995 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Mon Jun 12 15:01:03 1995 +0200
@@ -246,6 +246,7 @@
     val (symbs, lhs) = add_args raw_symbs typ pris;
     val copy_prod = lhs mem ["prop", "logic"]
           andalso const <> ""
+          andalso not (null symbs)
           andalso not (exists is_delim symbs);
     val lhs' = if convert andalso not copy_prod then
                  (if lhs mem logtypes then logic