# HG changeset patch
# User wenzelm
# Date 1142709050 -3600
# Node ID 798192b86c417c19fec7399add956cbfdd1935b7
# Parent  033c3ade1e8412af96dc77ad1982af3a5ade0705
made $$ and "this" monomorphic (string);

diff -r 033c3ade1e84 -r 798192b86c41 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sat Mar 18 20:10:49 2006 +0100
+++ b/src/Pure/General/scan.ML	Sat Mar 18 20:10:50 2006 +0100
@@ -28,7 +28,7 @@
   (*concatenation*)
   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
   (*one element literal*)
-  val $$ : ''a -> ''a list -> ''a * ''a list
+  val $$ : string -> string list -> string * string list
 end;
 
 signature SCAN =
@@ -39,7 +39,7 @@
   val succeed: 'a -> 'b -> 'a * 'b
   val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
   val one: ('a -> bool) -> 'a list -> 'a * 'a list
-  val this: ''a list -> ''a list -> ''a list * ''a list
+  val this: string list -> string list -> string list * string list
   val this_string: string -> string list -> string * string list
   val any: ('a -> bool) -> 'a list -> 'a list * 'a list
   val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
@@ -157,14 +157,14 @@
 
 fun $$ _ [] = raise MORE NONE
   | $$ a (x :: xs) =
-      if a = x then (x, xs) else raise FAIL NONE;
+      if (a: string) = x then (x, xs) else raise FAIL NONE;
 
 fun this ys xs =
   let
     fun drop_prefix [] xs = xs
       | drop_prefix (_ :: _) [] = raise MORE NONE
       | drop_prefix (y :: ys) (x :: xs) =
-          if y = x then drop_prefix ys xs else raise FAIL NONE;
+          if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
   in (ys, drop_prefix ys xs) end;
 
 fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)