@@ -739,7 +739,9 @@ rhs syn n = do lchar '='; expr syn
739 <|> do reserved "impossible"; return PImpossible
739 <|> do reserved "impossible"; return PImpossible
740 <?> "function right hand side"
740 <?> "function right hand side"
741 where mkN :: Name -> Name
741 where mkN :: Name -> Name
742+ mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
743+ then sUN "infix_op_lemma_1"
742− mkN (UN x) = sUN (str x++"_lemma_1")
744+ else sUN (str x++"_lemma_1")
743 mkN (NS x n) = NS (mkN x) n
745 mkN (NS x n) = NS (mkN x) n
744 n' :: Name
746 n' :: Name
745 n' = mkN n
747 n' = mkN n