fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified
authorclasohm
Mon, 12 Jun 1995 15:01:03 +0200
changeset 1145 d25b863ab2ac
parent 1144 5a62ecf80126
child 1146 75caf28a3aa9
fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified
src/Pure/Syntax/syn_ext.ML
--- 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