Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove newly added wrong logic
authorblanchet
Thu, 24 Mar 2011 17:49:27 +0100
changeset 42101 2c75267e7b8d
parent 42100 062381c5f9f8
child 42102 fcfd07f122d4
remove newly added wrong logic
src/HOL/Tools/Metis/metis_reconstruct.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle