| changeset 16861 | 7446b4be013b |
| parent 16787 | b6b6e2faaa41 |
| child 17018 | 1e9e0f5877f2 |
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 15 15:44:11 2005 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 15 15:44:15 2005 +0200 @@ -210,8 +210,7 @@ (**** eliminate definitions in proof ****) -fun vars_of t = rev (fold_aterms - (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []); +fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []); fun insert_refl defs Ts (prf1 %% prf2) = insert_refl defs Ts prf1 %% insert_refl defs Ts prf2