src/Pure/Proof/proof_rewrite_rules.ML
changeset 13917 a67c9e6570ac
parent 13646 46ed3d042ba5
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Apr 23 00:12:14 2003 +0200
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Apr 23 00:13:32 2003 +0200
     1.3 @@ -263,12 +263,21 @@
     1.4  fun elim_vars mk_default prf =
     1.5    let
     1.6      val prop = Reconstruct.prop_of prf;
     1.7 -    val vars = fold_proof_terms add_term_vars snd ([], prf) \\ term_vars prop;
     1.8 -    val inst = map (fn Var (ixn, T) => (ixn, list_abs
     1.9 -      (apfst (map (pair "x")) (apsnd mk_default (strip_type T))))) vars
    1.10 +    val tv = term_vars prop;
    1.11 +    val tf = term_frees prop;
    1.12 +
    1.13 +    fun mk_default' T = list_abs
    1.14 +      (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
    1.15 +
    1.16 +    fun elim_varst (t $ u) = elim_varst t $ elim_varst u
    1.17 +      | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
    1.18 +      | elim_varst (f as Free (_, T)) = if f mem tf then f else mk_default' T
    1.19 +      | elim_varst (v as Var (_, T)) = if v mem tv then v else mk_default' T
    1.20 +      | elim_varst t = t
    1.21    in
    1.22 -    norm_proof (Envir.Envir {iTs = Vartab.empty, asol = Vartab.make inst,
    1.23 -      maxidx = 0}) prf
    1.24 +    map_proof_terms (fn t => if not (null (term_vars t \\ tv)) orelse
    1.25 +        not (null (term_frees t \\ tf)) then Envir.beta_norm (elim_varst t)
    1.26 +      else t) I prf
    1.27    end;
    1.28  
    1.29  end;