src/Pure/Isar/token.ML
changeset 43947 9b00f09f7721
parent 43773 e8ba493027a3
child 44658 5bec9c15ef29
     1.1 --- a/src/Pure/Isar/token.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/Isar/token.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -50,7 +50,6 @@
     1.4    val assign: value option -> T -> unit
     1.5    val closure: T -> T
     1.6    val ident_or_symbolic: string -> bool
     1.7 -  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
     1.8    val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
     1.9    val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
    1.10      (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
    1.11 @@ -257,7 +256,7 @@
    1.12  
    1.13  open Basic_Symbol_Pos;
    1.14  
    1.15 -fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
    1.16 +fun !!! msg = Symbol_Pos.!!! (fn () => "Outer lexical error: " ^ msg);
    1.17  
    1.18  
    1.19  (* scan symbolic idents *)