src/Pure/Proof/extraction.ML
changeset 28375 c879d88d038a
parent 28370 37f56e6e702d
child 28674 08a77c495dc1
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Sep 26 17:24:15 2008 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Sep 26 19:07:56 2008 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    | rlz_proc _ = NONE;
     1.5  
     1.6  val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
     1.7 -  take_prefix (not o equal ":") o explode;
     1.8 +  take_prefix (fn s => s <> ":") o explode;
     1.9  
    1.10  type rules =
    1.11    {next: int, rs: ((term * term) list * (term * term)) list,
    1.12 @@ -259,7 +259,7 @@
    1.13  val add_typeof_eqns = gen_add_typeof_eqns read_condeq;
    1.14  
    1.15  fun thaw (T as TFree (a, S)) =
    1.16 -      if exists_string (equal ":") a then TVar (unpack_ixn a, S) else T
    1.17 +      if exists_string (fn s => s = ":") a then TVar (unpack_ixn a, S) else T
    1.18    | thaw (Type (a, Ts)) = Type (a, map thaw Ts)
    1.19    | thaw T = T;
    1.20  
    1.21 @@ -473,7 +473,7 @@
    1.22        in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    1.23  
    1.24      fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    1.25 -    fun find' s = map snd o List.filter (equal s o fst)
    1.26 +    fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
    1.27  
    1.28      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
    1.29        (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs