# HG changeset patch
# User blanchet
# Date 1305637896 -7200
# Node ID 1068d8fc1331b2e5b4cf0b703efd905a43b6b4a6
# Parent  1558741f8a72f39c56fc8e050740314e06791742
generate type classes predicates in new "shallow" encoding

diff -r 1558741f8a72 -r 1068d8fc1331 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 17 15:11:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 17 15:11:36 2011 +0200
@@ -1025,7 +1025,12 @@
       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
     val bounds = bound_names |> map (fn name => ATerm (name, []))
     fun const args = ATerm ((s, s'), map fo_term_from_typ T_args @ args)
-    fun eq tm1 tm2 = ATerm (`I "equal", [tm1, tm2])
+    val atomic_Ts = atyps_of T
+    fun eq tm1 tm2 =
+      ATerm (`I "equal", [tm1, tm2])
+      |> AAtom
+      |> bound_atomic_types type_sys atomic_Ts
+      |> close_formula_universally
     val should_encode =
       should_encode_type ctxt nonmono_Ts
           (if polymorphism_of_type_sys type_sys = Polymorphic then All_Types
@@ -1034,9 +1039,7 @@
     val add_formula_for_res =
       if should_encode res_T then
         cons (Formula (ident_base ^ "_res", Axiom,
-                       AAtom (eq (tag_with res_T (const bounds))
-                                 (const bounds))
-                       |> close_formula_universally,
+                       eq (tag_with res_T (const bounds)) (const bounds),
                        NONE, NONE))
       else
         I
@@ -1046,10 +1049,9 @@
           case chop k bounds of
             (bounds1, bound :: bounds2) =>
             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), Axiom,
-                           AAtom (eq (const (bounds1 @
-                                  tag_with arg_T bound :: bounds2))
-                                     (const bounds))
-                           |> close_formula_universally,
+                           eq (const (bounds1 @ tag_with arg_T bound ::
+                                      bounds2))
+                              (const bounds),
                            NONE, NONE))
           | _ => raise Fail "expected nonempty tail"
         else