# HG changeset patch
# User blanchet
# Date 1304555222 -7200
# Node ID 4d29b4785f435d27c1180c852d39a76638cdd14a
# Parent  e38590764c34fc9182579437c97a488a3bbbe2bf
removed unsound hAPP optimization

diff -r e38590764c34 -r 4d29b4785f43 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 00:51:56 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 02:27:02 2011 +0200
@@ -637,43 +637,29 @@
       | (head, args) => list_explicit_app head (map aux args)
   in aux end
 
-fun impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
+fun impose_type_arg_policy_in_combterm type_sys =
   let
     fun aux (CombApp tmp) = CombApp (pairself aux tmp)
       | aux (CombConst (name as (s, _), T, T_args)) =
-        let
-          val level = level_of_type_sys type_sys
-          val (T, T_args) =
-            (* avoid needless identical homogenized versions of "hAPP" *)
-            if s = const_prefix ^ explicit_app_base then
-              T_args |> map (homogenized_type ctxt nonmono_Ts level)
-                     |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
-                                    (T --> T, Ts)
-                                  end)
-            else
-              (T, T_args)
-        in
-          (case strip_prefix_and_unascii const_prefix s of
-             NONE => (name, T_args)
-           | SOME s'' =>
-             let val s'' = invert_const s'' in
-               case type_arg_policy type_sys s'' of
-                 No_Type_Args => (name, [])
-               | Explicit_Type_Args => (name, T_args)
-               | Mangled_Type_Args => (mangled_const_name T_args name, [])
-             end)
-          |> (fn (name, T_args) => CombConst (name, T, T_args))
-        end
+        (case strip_prefix_and_unascii const_prefix s of
+           NONE => (name, T_args)
+         | SOME s'' =>
+           let val s'' = invert_const s'' in
+             case type_arg_policy type_sys s'' of
+               No_Type_Args => (name, [])
+             | Explicit_Type_Args => (name, T_args)
+             | Mangled_Type_Args => (mangled_const_name T_args name, [])
+           end)
+        |> (fn (name, T_args) => CombConst (name, T, T_args))
       | aux tm = tm
   in aux end
 
-fun repair_combterm ctxt nonmono_Ts type_sys sym_tab =
+fun repair_combterm type_sys sym_tab =
   introduce_explicit_apps_in_combterm sym_tab
   #> introduce_predicators_in_combterm sym_tab
-  #> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
-fun repair_fact ctxt nonmono_Ts type_sys sym_tab =
-  update_combformula (formula_map
-      (repair_combterm ctxt nonmono_Ts type_sys sym_tab))
+  #> impose_type_arg_policy_in_combterm type_sys
+fun repair_fact type_sys sym_tab =
+  update_combformula (formula_map (repair_combterm type_sys sym_tab))
 
 (** Helper facts **)
 
@@ -757,17 +743,17 @@
 
 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
 
-fun type_pred_combatom ctxt nonmono_Ts type_sys T tm =
+fun type_pred_combatom type_sys T tm =
   CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
            tm)
-  |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
+  |> impose_type_arg_policy_in_combterm type_sys
   |> AAtom
 
 fun formula_from_combformula ctxt nonmono_Ts type_sys =
   let
     fun tag_with_type type_sys T tm =
       CombConst (`make_fixed_const type_tag_name, T --> T, [T])
-      |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
+      |> impose_type_arg_policy_in_combterm type_sys
       |> do_term true
       |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
     and do_term top_level u =
@@ -795,7 +781,7 @@
       | _ => K NONE
     fun do_out_of_bound_type (s, T) =
       if should_predicate_on_type ctxt nonmono_Ts type_sys T then
-        type_pred_combatom ctxt nonmono_Ts type_sys T (CombVar (s, T))
+        type_pred_combatom type_sys T (CombVar (s, T))
         |> do_formula |> SOME
       else
         NONE
@@ -978,7 +964,7 @@
              (if n > 1 then "_" ^ string_of_int j else ""), Axiom,
              CombConst ((s, s'), T, T_args)
              |> fold (curry (CombApp o swap)) bound_tms
-             |> type_pred_combatom ctxt nonmono_Ts type_sys res_T
+             |> type_pred_combatom type_sys res_T
              |> mk_aquant AForall (bound_names ~~ bound_Ts)
              |> formula_from_combformula ctxt nonmono_Ts type_sys
              |> close_formula_universally,
@@ -1053,7 +1039,7 @@
     val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
     val nonmono_Ts =
       [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
-    val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
+    val repair = repair_fact type_sys sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
     val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
     val helpers =