equal
deleted
inserted
replaced
134 |
134 |
135 fun strip_abs 0 t = t |
135 fun strip_abs 0 t = t |
136 | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t |
136 | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t |
137 | strip_abs _ _ = error "strip_abs: not an abstraction"; |
137 | strip_abs _ _ = error "strip_abs: not an abstraction"; |
138 |
138 |
139 fun prf_subst_TVars tye = |
139 val prf_subst_TVars = map_proof_types o typ_subst_TVars; |
140 map_proof_terms (subst_TVars tye) (typ_subst_TVars tye); |
|
141 |
140 |
142 fun relevant_vars types prop = List.foldr (fn |
141 fun relevant_vars types prop = List.foldr (fn |
143 (Var ((a, _), T), vs) => (case strip_type T of |
142 (Var ((a, _), T), vs) => (case strip_type T of |
144 (_, Type (s, _)) => if member (op =) types s then a :: vs else vs |
143 (_, Type (s, _)) => if member (op =) types s then a :: vs else vs |
145 | _ => vs) |
144 | _ => vs) |