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_atp_translate.ML
changeset 40145 04a05b2a7a36
parent 40114 acb75271cdce
child 40204 da97d75e20e6 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Oct 26 10:39:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Oct 26 10:57:04 2010 +0200
@@ -53,7 +53,7 @@
 
 fun combformula_for_prop thy =
   let
-    val do_term = combterm_from_term thy ~1
+    val do_term = combterm_from_term thy
     fun do_quant bs q s T t' =
       let val s = Name.variant (map fst bs) s in
         do_formula ((s, T) :: bs) t'
isabelle