# HG changeset patch
# User steckerm
# Date 1411202663 -7200
# Node ID c3c7a09a3adaaaf36b6de336500d90d9f0828c2c
# Parent  4be5ab4452f41b7a1347e83e6bef88fd3bc82975
Made encoded type for apply less restrictive

diff -r 4be5ab4452f4 -r c3c7a09a3ada src/HOL/Tools/ATP/atp_waldmeister.ML
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:44:23 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:44:23 2014 +0200
@@ -201,7 +201,7 @@
 
 end;
 
-structure ATP_Waldmeister : ATP_WALDMEISTER  =
+structure ATP_Waldmeister (*** : ATP_WALDMEISTER  *) =
 struct
 
 open ATP_Util
@@ -301,9 +301,10 @@
     let
       val funT = type_of function
       val argT = type_of a
-      val newT = funT --> argT --> (dest_funT funT |> snd)
+      val resT = dest_funT funT |> snd
+      val newT = funT --> argT --> resT
     in
-      mk_waldmeister_app (Const (waldmeister_apply ^ encode_type newT, newT) $ function $ a) args
+      mk_waldmeister_app (Const (waldmeister_apply ^ encode_type resT, newT) $ function $ a) args
     end
 
 fun hide_partial_applications info (trm as (_ $ _)) =