Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 37512 ff72d3ddc898
parent 37509 f39464d971c4
child 37515 ef3742657bc6 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Jun 23 09:40:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Jun 23 10:20:33 2010 +0200
@@ -166,7 +166,6 @@
       fun aux skolem_somes
               (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
           let
-            val t = Envir.beta_eta_contract t
             val (skolem_somes, s) =
               if i = ~1 then
                 (skolem_somes, @{const_name undefined})
isabelle