remove (op =);
authorwenzelm
Tue Mar 21 12:18:13 2006 +0100 (2006-03-21)
changeset 1930415f001295a7b
parent 19303 7da7e96bd74d
child 19305 5c16895d548b
remove (op =);
tuned;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Tue Mar 21 12:18:11 2006 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Tue Mar 21 12:18:13 2006 +0100
     1.3 @@ -164,7 +164,7 @@
     1.4    | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab =>
     1.5        case Symtab.lookup tab s of
     1.6          NONE => thms_of_proof prf (Symtab.update (s, [(prop, prf')]) tab)
     1.7 -      | SOME ps => if exists (equal prop o fst) ps then tab else
     1.8 +      | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
     1.9            thms_of_proof prf (Symtab.update (s, (prop, prf')::ps) tab))
    1.10    | thms_of_proof (MinProof (prfs, _, _)) = fold (thms_of_proof o proof_of_min_thm) prfs
    1.11    | thms_of_proof _ = I;
    1.12 @@ -572,7 +572,8 @@
    1.13  
    1.14  fun varify_proof t fixed prf =
    1.15    let
    1.16 -    val fs = add_term_tfrees (t, []) \\ fixed;
    1.17 +    val fs = Term.fold_types (Term.fold_atyps
    1.18 +      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    1.19      val ixns = add_term_tvar_ixns (t, []);
    1.20      val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
    1.21      fun thaw (f as (a, S)) =
    1.22 @@ -702,7 +703,7 @@
    1.23    | flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) =
    1.24        Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k))
    1.25    | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
    1.26 -      map Bound (j-1 downto 0)), map PBound (i-1 downto 0 \ i-n));
    1.27 +      map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
    1.28  
    1.29  fun bicompose_proof flatten Bs oldAs newAs A n rprf sprf =
    1.30    let