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.
I have an intuition that it's sound to omit the first type arg of an hAPP -- and this reduces the size of monomorphized problems quite a bit
authorblanchet
Thu, 05 May 2011 08:03:28 +0200
changeset 42691 6efda6167e5d
parent 42690 4d29b4785f43
child 42692 60359df11dc4
I have an intuition that it's sound to omit the first type arg of an hAPP -- and this reduces the size of monomorphized problems quite a bit
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 02:27:02 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 08:03:28 2011 +0200
@@ -618,10 +618,10 @@
 fun explicit_app arg head =
   let
     val head_T = combtyp_of head
-    val (arg_T, res_T) = dest_funT head_T
+    val (_, res_T) = dest_funT head_T
     val explicit_app =
       CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
-                 [arg_T, res_T])
+                 [res_T])
   in list_app explicit_app [head, arg] end
 fun list_explicit_app head args = fold explicit_app args head
isabelle