# HG changeset patch
# User blanchet
# Date 1305793453 -7200
# Node ID 40649ab0ceada11cb5167c48ba1f917763e9d581
# Parent  3bb63850488b1d29d2411798e9645f83d8a32402
honor "conj_sym_kind" also for tag symbol declarations

diff -r 3bb63850488b -r 40649ab0cead src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 19 10:24:13 2011 +0200
@@ -1045,11 +1045,14 @@
              NONE, NONE)
   end
 
-fun formula_lines_for_tag_sym_decl ctxt nonmono_Ts type_sys n s
-                                   (j, (s', T_args, T, pred_sym, ary, _)) =
+fun formula_lines_for_tag_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s
+                                  (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   let
     val ident_base =
       sym_decl_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
+    val (kind, maybe_negate) =
+      if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
+      else (Axiom, I)
     val (arg_Ts, res_T) = chop_fun ary T
     val bound_names =
       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
@@ -1061,11 +1064,12 @@
        else AAtom (ATerm (`I "equal", tms)))
       |> bound_atomic_types type_sys atomic_Ts
       |> close_formula_universally
+      |> maybe_negate
     val should_encode = should_encode_type ctxt nonmono_Ts All_Types
     val tag_with = tag_with_type ctxt nonmono_Ts type_sys
     val add_formula_for_res =
       if should_encode res_T then
-        cons (Formula (ident_base ^ "_res", Axiom,
+        cons (Formula (ident_base ^ "_res", kind,
                        eq [tag_with res_T (const bounds), const bounds],
                        NONE, NONE))
       else
@@ -1075,7 +1079,7 @@
         if should_encode arg_T then
           case chop k bounds of
             (bounds1, bound :: bounds2) =>
-            cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), Axiom,
+            cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
                            eq [const (bounds1 @ tag_with arg_T bound ::
                                       bounds2),
                                const bounds],
@@ -1124,7 +1128,8 @@
      | Light =>
        let val n = length decls in
          (0 upto n - 1 ~~ decls)
-         |> maps (formula_lines_for_tag_sym_decl ctxt nonmono_Ts type_sys n s)
+         |> maps (formula_lines_for_tag_sym_decl ctxt conj_sym_kind nonmono_Ts
+                                                 type_sys n s)
        end)
 
 fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys