src/Pure/Syntax/syn_ext.ML
changeset 1145 d25b863ab2ac
parent 922 196ca0973a6d
child 1178 b28c6ecc3e6d
equal deleted inserted replaced
1144:5a62ecf80126 1145:d25b863ab2ac
   244 
   244 
   245     val raw_symbs = scan_symbs (explode sy);
   245     val raw_symbs = scan_symbs (explode sy);
   246     val (symbs, lhs) = add_args raw_symbs typ pris;
   246     val (symbs, lhs) = add_args raw_symbs typ pris;
   247     val copy_prod = lhs mem ["prop", "logic"]
   247     val copy_prod = lhs mem ["prop", "logic"]
   248           andalso const <> ""
   248           andalso const <> ""
       
   249           andalso not (null symbs)
   249           andalso not (exists is_delim symbs);
   250           andalso not (exists is_delim symbs);
   250     val lhs' = if convert andalso not copy_prod then
   251     val lhs' = if convert andalso not copy_prod then
   251                  (if lhs mem logtypes then logic
   252                  (if lhs mem logtypes then logic
   252                   else if lhs = "prop" then sprop else lhs)
   253                   else if lhs = "prop" then sprop else lhs)
   253                else lhs;
   254                else lhs;