# HG changeset patch
# User blanchet
# Date 1300985367 -3600
# Node ID 2c75267e7b8d33a69e5d8e29ae5fae6230f2f2d6
# Parent  062381c5f9f8b2d88ef1d80640a33bf8fa067932
remove newly added wrong logic

diff -r 062381c5f9f8 -r 2c75267e7b8d src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -658,7 +658,6 @@
     fun do_instantiate th =
       let
         val var = Term.add_vars (prop_of th) []
-                  |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
                   |> the_single
       in th |> term_instantiate thy [(Var var, t')] end
   in