src/Pure/proofterm.ML

   let
     val fs = add_term_tfrees (t, []) \\ fixed;
     val ixns = add_term_tvar_ixns (t, []);
     val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
     fun thaw (f as (a, S)) =
-      (case assoc (fmap, f) of
+      (case gen_assoc (op =) (fmap, f) of
         NONE => TFree f
       | SOME b => TVar ((b, 0), S));
   in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
   end;
 

           | NONE => NONE)
       | rew2 _ _ _ = NONE
 
   in getOpt (rew1 [] skel0 prf, prf) end;
 
-fun rewrite_proof tsig = rewrite_prf (fn (tab, f) =>
-  Type.typ_match tsig (tab, f ()) handle Type.TYPE_MATCH => raise PMatch);
+fun rewrite_proof tsig = rewrite_prf (fn (tyenv, f) =>
+  Type.typ_match tsig (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
 
 fun rewrite_proof_notypes rews = rewrite_prf fst rews;
 
+
 (**** theory data ****)
-
-(* data kind 'Pure/proof' *)
 
 structure ProofData = TheoryDataFun
 (struct
   val name = "Pure/proof";
   type T = ((proof * proof) list *