src/Pure/Syntax/syn_ext.ML
changeset 5870 5d4fc952be47
parent 5690 4b056ee5435c
child 6322 7047300264c9
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon Nov 16 10:41:08 1998 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Nov 16 10:41:27 1998 +0100
     1.3 @@ -187,7 +187,7 @@
     1.4      $$ "'" -- Scan.one Symbol.is_blank >> K None;
     1.5  
     1.6    val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
     1.7 -  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.stopper scan_symbs);
     1.8 +  val read_symbs = mapfilter I o the o Scan.read Symbol.stopper scan_symbs;
     1.9  in
    1.10    val read_mixfix = read_symbs o Symbol.explode;
    1.11  end;