# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID d9963b253ffa4e41e108eeb5e62587470a850a0b
# Parent  e155be7125bacfbd8acfd3e59732d173fee9b060
fix handling of proxies after recent drastic changes to the type encodings

diff -r e155be7125ba -r d9963b253ffa src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -484,19 +484,20 @@
     full_types orelse is_combtyp_dangerous ctxt ty
   | should_tag_with_type _ _ _ = false
 
-val fname_table =
-  [("c_False", (0, ("c_fFalse", @{const_name Metis.fFalse}))),
-   ("c_True", (0, ("c_fTrue", @{const_name Metis.fTrue}))),
-   ("c_Not", (1, ("c_fNot", @{const_name Metis.fNot}))),
-   ("c_conj", (2, ("c_fconj", @{const_name Metis.fconj}))),
-   ("c_disj", (2, ("c_fdisj", @{const_name Metis.fdisj}))),
-   ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
-   ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
+val proxy_table =
+  [("c_False", ("c_fFalse", @{const_name Metis.fFalse})),
+   ("c_True", ("c_fTrue", @{const_name Metis.fTrue})),
+   ("c_Not", ("c_fNot", @{const_name Metis.fNot})),
+   ("c_conj", ("c_fconj", @{const_name Metis.fconj})),
+   ("c_disj", ("c_fdisj", @{const_name Metis.fdisj})),
+   ("c_implies", ("c_fimplies", @{const_name Metis.fimplies})),
+   ("equal", ("c_fequal", @{const_name Metis.fequal}))]
 
 fun repair_combterm_consts type_sys =
   let
-    fun aux (CombApp tmp) = CombApp (pairself aux tmp)
-      | aux (CombConst (name as (s, _), ty, ty_args)) =
+    fun aux top_level (CombApp (tm1, tm2)) =
+        CombApp (aux top_level tm1, aux false tm2)
+      | aux top_level (CombConst (name as (s, _), ty, ty_args)) =
         (case strip_prefix_and_unascii const_prefix s of
            NONE => (name, ty_args)
          | SOME s'' =>
@@ -506,9 +507,20 @@
              | Mangled_Types => (mangled_const_name ty_args name, [])
              | Explicit_Type_Args => (name, ty_args)
            end)
+        |> (fn (name as (s, s'), ty_args) =>
+               case AList.lookup (op =) proxy_table s of
+                 SOME proxy_name =>
+                 if top_level then
+                   (case s of
+                      "c_False" => ("$false", s')
+                    | "c_True" => ("$true", s')
+                    | _ => name, [])
+                  else
+                    (proxy_name, ty_args)
+                | NONE => (name, ty_args))
         |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
-      | aux tm = tm
-  in aux end
+      | aux _ tm = tm
+  in aux true end
 
 fun pred_combtyp ty =
   case combtyp_from_typ @{typ "unit => bool"} of
@@ -523,26 +535,15 @@
 
 fun formula_for_combformula ctxt type_sys =
   let
-    fun do_term top_level u =
+    fun do_term u =
       let
         val (head, args) = strip_combterm_comb u
         val (x, ty_args) =
           case head of
-            CombConst (name as (s, s'), _, ty_args) =>
-            (case AList.lookup (op =) fname_table s of
-               SOME (n, fname) =>
-               (if top_level andalso length args = n then
-                  case s of
-                    "c_False" => ("$false", s')
-                  | "c_True" => ("$true", s')
-                  | _ => name
-                else
-                  fname, [])
-             | NONE => (name, ty_args))
+            CombConst (name, _, ty_args) => (name, ty_args)
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
-        val t = ATerm (x, map fo_term_for_combtyp ty_args @
-                          map (do_term false) args)
+        val t = ATerm (x, map fo_term_for_combtyp ty_args @ map do_term args)
         val ty = combtyp_of u
       in
         t |> (if should_tag_with_type ctxt type_sys ty then
@@ -568,7 +569,7 @@
                            | (s, SOME ty) => do_out_of_bound_type (s, ty)) xs)
                     (do_formula phi))
       | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
-      | do_formula (AAtom tm) = AAtom (do_term true tm)
+      | do_formula (AAtom tm) = AAtom (do_term tm)
   in do_formula end
 
 fun formula_for_fact ctxt type_sys