diff -r 080c0006e917 -r 1a29ea173bf9 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:24:44 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:38:51 2014 +0100
@@ -9,6 +9,7 @@
   type T = Symbol.symbol * Position.T
   val symbol: T -> Symbol.symbol
   val $$ : Symbol.symbol -> T list -> T * T list
+  val ~$$ : Symbol.symbol -> T list -> T * T list
   val $$$ : Symbol.symbol -> T list -> T list * T list
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
   val content: T list -> string
@@ -87,6 +88,8 @@
 fun change_prompt scan = Scan.prompt "# " scan;
 
 fun $$ s = Scan.one (fn x => symbol x = s);
+fun ~$$ s = Scan.one (fn x => symbol x <> s);
+
 fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
 fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
 
@@ -278,6 +281,7 @@
 structure Basic_Symbol_Pos =   (*not open by default*)
 struct
   val $$ = Symbol_Pos.$$;
+  val ~$$ = Symbol_Pos.~$$;
   val $$$ = Symbol_Pos.$$$;
   val ~$$$ = Symbol_Pos.~$$$;
 end;