1.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Jun 06 10:40:01 1995 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Jun 12 15:01:03 1995 +0200
     1.3 @@ -246,6 +246,7 @@
     1.4      val (symbs, lhs) = add_args raw_symbs typ pris;
     1.5      val copy_prod = lhs mem ["prop", "logic"]
     1.6            andalso const <> ""
     1.7 +          andalso not (null symbs)
     1.8            andalso not (exists is_delim symbs);
     1.9      val lhs' = if convert andalso not copy_prod then
    1.10                   (if lhs mem logtypes then logic