src/Pure/Proof/extraction.ML
changeset 36620 e6bb250402b5
parent 36042 85efdadee8ae
child 36744 6e1f3d609a68
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue May 04 11:02:50 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue May 04 12:30:15 2010 +0200
     1.3 @@ -136,8 +136,7 @@
     1.4    | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
     1.5    | strip_abs _ _ = error "strip_abs: not an abstraction";
     1.6  
     1.7 -fun prf_subst_TVars tye =
     1.8 -  map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
     1.9 +val prf_subst_TVars = map_proof_types o typ_subst_TVars;
    1.10  
    1.11  fun relevant_vars types prop = List.foldr (fn
    1.12        (Var ((a, _), T), vs) => (case strip_type T of