--- a/src/Pure/Syntax/syn_ext.ML Thu Sep 21 19:05:41 2006 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Thu Sep 21 19:05:56 2006 +0200
@@ -194,7 +194,7 @@
local
-fun is_meta c = c mem ["(", ")", "/", "_", "\\<index>"];
+val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
val scan_delim_char =
$$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
@@ -308,7 +308,7 @@
val (symbs, lhs) = add_args raw_symbs typ' pris;
val copy_prod =
- lhs mem ["prop", "logic"]
+ (lhs = "prop" orelse lhs = "logic")
andalso const <> ""
andalso not (null symbs)
andalso not (exists is_delim symbs);