# HG changeset patch
# User berghofe
# Date 1033396857 -7200
# Node ID 9a6f43b8eae1fa9fb869505bc0ba8a9b59235c3f
# Parent  6908230623a30632318d633d1722f659798f05f3
Added function elim_vars.

diff -r 6908230623a3 -r 9a6f43b8eae1 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Mon Sep 30 16:38:22 2002 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Mon Sep 30 16:40:57 2002 +0200
@@ -12,6 +12,7 @@
   val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
   val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
   val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
+  val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
   val setup : (theory -> theory) list
 end;
 
@@ -256,4 +257,18 @@
       (insert_refl defnames [] (f prf))
   end;
 
+
+(**** eliminate all variables that don't occur in the proposition ****)
+
+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
+  in
+    norm_proof (Envir.Envir {iTs = Vartab.empty, asol = Vartab.make inst,
+      maxidx = 0}) prf
+  end;
+
 end;