member (op =);
authorwenzelm
Thu Sep 21 19:05:56 2006 +0200 (2006-09-21)
changeset 20675cb19d18aef01
parent 20674 93baed0f741c
child 20676 21e096f30c5d
member (op =);
tuned;
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/Proof/reconstruct.ML	Thu Sep 21 19:05:41 2006 +0200
     1.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu Sep 21 19:05:56 2006 +0200
     1.3 @@ -232,23 +232,26 @@
     1.4        | mk_cnstrts _ _ _ _ _ = error "reconstruct_proof: minimal proof object"
     1.5    in mk_cnstrts env [] [] Symtab.empty cprf end;
     1.6  
     1.7 -fun add_term_ixns (is, t) = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I) t is;
     1.8 -
     1.9  
    1.10  (**** update list of free variables of constraints ****)
    1.11  
    1.12 +val add_term_ixns = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
    1.13 +val add_typ_ixns = fold_atyps (fn TVar (ai, _) => insert (op =) ai | _ => I);
    1.14 +
    1.15  fun upd_constrs env cs =
    1.16    let
    1.17      val Envir.Envir {asol, iTs, ...} = env;
    1.18 -    val dom = Vartab.foldl (uncurry (cons o fst) o Library.swap)
    1.19 -      (Vartab.foldl (uncurry (cons o fst) o Library.swap) ([], asol), iTs); 
    1.20 -    val vran = Vartab.foldl (add_typ_ixns o apsnd (snd o snd))
    1.21 -      (Vartab.foldl (add_term_ixns o apsnd (snd o snd)) ([], asol), iTs);
    1.22 +    val dom = []
    1.23 +      |> Vartab.fold (cons o #1) asol
    1.24 +      |> Vartab.fold (cons o #1) iTs;
    1.25 +    val vran = []
    1.26 +      |> Vartab.fold (add_term_ixns o #2 o #2) asol
    1.27 +      |> Vartab.fold (add_typ_ixns o #2 o #2) iTs;
    1.28      fun check_cs [] = []
    1.29        | check_cs ((u, p, vs)::ps) =
    1.30            let val vs' = subtract (op =) dom vs;
    1.31            in if vs = vs' then (u, p, vs)::check_cs ps
    1.32 -             else (true, p, vs' union vran)::check_cs ps
    1.33 +             else (true, p, fold (insert (op =)) vs' vran)::check_cs ps
    1.34            end
    1.35    in check_cs cs end;
    1.36  
    1.37 @@ -376,7 +379,7 @@
    1.38              val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
    1.39                (term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
    1.40              val varify = map_type_tfree (fn p as (a, S) =>
    1.41 -              if p mem tfrees then TVar ((a, ~1), S) else TFree p)
    1.42 +              if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
    1.43            in
    1.44              (maxidx', prfs', map_proof_terms (subst_TVars tye o
    1.45                 map_types varify) (typ_subst_TVars tye o varify) prf)
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Sep 21 19:05:41 2006 +0200
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Sep 21 19:05:56 2006 +0200
     2.3 @@ -194,7 +194,7 @@
     2.4  
     2.5  local
     2.6  
     2.7 -fun is_meta c = c mem ["(", ")", "/", "_", "\\<index>"];
     2.8 +val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
     2.9  
    2.10  val scan_delim_char =
    2.11    $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
    2.12 @@ -308,7 +308,7 @@
    2.13      val (symbs, lhs) = add_args raw_symbs typ' pris;
    2.14  
    2.15      val copy_prod =
    2.16 -      lhs mem ["prop", "logic"]
    2.17 +      (lhs = "prop" orelse lhs = "logic")
    2.18          andalso const <> ""
    2.19          andalso not (null symbs)
    2.20          andalso not (exists is_delim symbs);