src/Pure/Proof/extraction.ML
changeset 40844 5895c525739d
parent 40627 becf5d5187cc
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Dec 01 15:02:39 2010 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Dec 01 15:03:44 2010 +0100
     1.3 @@ -135,11 +135,13 @@
     1.4  
     1.5  val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars;
     1.6  
     1.7 -fun relevant_vars types prop = List.foldr (fn
     1.8 -      (Var ((a, _), T), vs) => (case strip_type T of
     1.9 -        (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
    1.10 -      | _ => vs)
    1.11 -    | (_, vs) => vs) [] (vars_of prop);
    1.12 +fun relevant_vars types prop =
    1.13 +  List.foldr
    1.14 +    (fn (Var ((a, _), T), vs) =>
    1.15 +        (case body_type T of
    1.16 +          Type (s, _) => if member (op =) types s then a :: vs else vs
    1.17 +        | _ => vs)
    1.18 +      | (_, vs) => vs) [] (vars_of prop);
    1.19  
    1.20  fun tname_of (Type (s, _)) = s
    1.21    | tname_of _ = "";