# HG changeset patch
# User clasohm
# Date 802962063 -7200
# Node ID d25b863ab2acf817f0265afa16cf740fbda7a47b
# Parent  5a62ecf80126458d16d8a6b969eee5716ad624e0
fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified

diff -r 5a62ecf80126 -r d25b863ab2ac 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