diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -70,7 +70,7 @@
   | rlz_proc _ = NONE;
 
 val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
-  take_prefix (not o equal ":") o explode;
+  take_prefix (fn s => s <> ":") o explode;
 
 type rules =
   {next: int, rs: ((term * term) list * (term * term)) list,
@@ -259,7 +259,7 @@
 val add_typeof_eqns = gen_add_typeof_eqns read_condeq;
 
 fun thaw (T as TFree (a, S)) =
-      if exists_string (equal ":") a then TVar (unpack_ixn a, S) else T
+      if exists_string (fn s => s = ":") a then TVar (unpack_ixn a, S) else T
   | thaw (Type (a, Ts)) = Type (a, map thaw Ts)
   | thaw T = T;
 
@@ -473,7 +473,7 @@
       in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
 
     fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
-    fun find' s = map snd o List.filter (equal s o fst)
+    fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
 
     fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
       (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs