# HG changeset patch
# User wenzelm
# Date 1142939893 -3600
# Node ID 15f001295a7ba24be67fe93c8f98724645f5b9b5
# Parent  7da7e96bd74dce93e741fd0692b2ea0577fcbe25
remove (op =);
tuned;

diff -r 7da7e96bd74d -r 15f001295a7b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Mar 21 12:18:11 2006 +0100
+++ b/src/Pure/proofterm.ML	Tue Mar 21 12:18:13 2006 +0100
@@ -164,7 +164,7 @@
   | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab =>
       case Symtab.lookup tab s of
         NONE => thms_of_proof prf (Symtab.update (s, [(prop, prf')]) tab)
-      | SOME ps => if exists (equal prop o fst) ps then tab else
+      | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
           thms_of_proof prf (Symtab.update (s, (prop, prf')::ps) tab))
   | thms_of_proof (MinProof (prfs, _, _)) = fold (thms_of_proof o proof_of_min_thm) prfs
   | thms_of_proof _ = I;
@@ -572,7 +572,8 @@
 
 fun varify_proof t fixed prf =
   let
-    val fs = add_term_tfrees (t, []) \\ fixed;
+    val fs = Term.fold_types (Term.fold_atyps
+      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
     val ixns = add_term_tvar_ixns (t, []);
     val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
     fun thaw (f as (a, S)) =
@@ -702,7 +703,7 @@
   | flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) =
       Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k))
   | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
-      map Bound (j-1 downto 0)), map PBound (i-1 downto 0 \ i-n));
+      map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
 
 fun bicompose_proof flatten Bs oldAs newAs A n rprf sprf =
   let