# HG changeset patch # User berghofe # Date 1051049612 -7200 # Node ID a67c9e6570ac4d67ed0841d41cc5679e02a5f843 # Parent f078a758e5d86335f280ff4437d73e8c1cedbc70 elim_vars now handles both Vars and Frees. diff -r f078a758e5d8 -r a67c9e6570ac src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Wed Apr 23 00:12:14 2003 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Wed Apr 23 00:13:32 2003 +0200 @@ -263,12 +263,21 @@ fun elim_vars mk_default prf = let val prop = Reconstruct.prop_of prf; - val vars = fold_proof_terms add_term_vars snd ([], prf) \\ term_vars prop; - val inst = map (fn Var (ixn, T) => (ixn, list_abs - (apfst (map (pair "x")) (apsnd mk_default (strip_type T))))) vars + val tv = term_vars prop; + val tf = term_frees prop; + + fun mk_default' T = list_abs + (apfst (map (pair "x")) (apsnd mk_default (strip_type T))); + + fun elim_varst (t $ u) = elim_varst t $ elim_varst u + | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t) + | elim_varst (f as Free (_, T)) = if f mem tf then f else mk_default' T + | elim_varst (v as Var (_, T)) = if v mem tv then v else mk_default' T + | elim_varst t = t in - norm_proof (Envir.Envir {iTs = Vartab.empty, asol = Vartab.make inst, - maxidx = 0}) prf + map_proof_terms (fn t => if not (null (term_vars t \\ tv)) orelse + not (null (term_frees t \\ tf)) then Envir.beta_norm (elim_varst t) + else t) I prf end; end;