# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID f65e5f0341b89603332c1de1dbe9636d9d0ce566
# Parent  2570e1a5ddfbbdab2d7028dc7cbf21308f3ebb8e
fixed "tags" type encoding after latest round of changes

diff -r 2570e1a5ddfb -r f65e5f0341b8 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
@@ -535,7 +535,7 @@
 
 fun formula_for_combformula ctxt type_sys =
   let
-    fun do_term u =
+    fun do_term top_level u =
       let
         val (head, args) = strip_combterm_comb u
         val (x, ty_args) =
@@ -543,10 +543,12 @@
             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 args)
+        val t = ATerm (x, map fo_term_for_combtyp ty_args @
+                          map (do_term false) args)
         val ty = combtyp_of u
       in
-        t |> (if should_tag_with_type ctxt type_sys ty then
+        t |> (if not top_level andalso
+                 should_tag_with_type ctxt type_sys ty then
                 tag_with_type (fo_term_for_combtyp ty)
               else
                 I)
@@ -569,7 +571,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 tm)
+      | do_formula (AAtom tm) = AAtom (do_term true tm)
   in do_formula end
 
 fun formula_for_fact ctxt type_sys
@@ -746,7 +748,7 @@
   in aux end
 
 fun repair_combterm thy type_sys sym_tab =
-  (case type_sys of Tags _ => I | _ => repair_pred_syms_in_combterm sym_tab)
+  repair_pred_syms_in_combterm sym_tab
   #> repair_apps_in_combterm thy type_sys sym_tab
   #> repair_combterm_consts type_sys
 val repair_combformula = formula_map ooo repair_combterm