# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID b9754f26c7bcbfa8c0d647427b61b2127ac30bd7
# Parent  ea2a28b1938f161e039e392d285faaa7a6ee69ef
handle special constants correctly in Isar proof reconstruction code, especially type predicates

diff -r ea2a28b1938f -r b9754f26c7bc src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
@@ -356,29 +356,33 @@
               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
           end
         | SOME b =>
-          if b = boolify_base then
-            aux (SOME @{typ bool}) [] (hd us)
-          else if b = explicit_app_base then
-            aux opt_T (nth us 1 :: extra_us) (hd us)
-          else
-            let
-              val (c, mangled_us) = b |> unmangled_const |>> invert_const
-              val num_ty_args = num_atp_type_args thy type_sys c
-              val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
-              (* Extra args from "hAPP" come after any arguments given directly
-                 to the constant. *)
-              val term_ts = map (aux NONE []) term_us
-              val extra_ts = map (aux NONE []) extra_us
-              val T =
-                case opt_T of
-                  SOME T => map fastype_of term_ts ---> T
-                | NONE =>
-                  if num_type_args thy c = length type_us then
-                    Sign.const_instance thy (c,
-                        map (type_from_fo_term tfrees) type_us)
-                  else
-                    HOLogic.typeT
-            in list_comb (Const (c, T), term_ts @ extra_ts) end
+          let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
+            if b = boolify_base then
+              aux (SOME @{typ bool}) [] (hd us)
+            else if b = explicit_app_base then
+              aux opt_T (nth us 1 :: extra_us) (hd us)
+            else if b = type_pred_base then
+              @{const True}
+            else
+              let
+                val num_ty_args = num_atp_type_args thy type_sys b
+                val (type_us, term_us) =
+                  chop num_ty_args us |>> append mangled_us
+                (* Extra args from "hAPP" come after any arguments given
+                   directly to the constant. *)
+                val term_ts = map (aux NONE []) term_us
+                val extra_ts = map (aux NONE []) extra_us
+                val T =
+                  case opt_T of
+                    SOME T => map fastype_of term_ts ---> T
+                  | NONE =>
+                    if num_type_args thy b = length type_us then
+                      Sign.const_instance thy
+                          (b, map (type_from_fo_term tfrees) type_us)
+                    else
+                      HOLogic.typeT
+              in list_comb (Const (b, T), term_ts @ extra_ts) end
+          end
         | NONE => (* a free or schematic variable *)
           let
             val ts = map (aux NONE []) (us @ extra_us)
diff -r ea2a28b1938f -r b9754f26c7bc 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
@@ -23,6 +23,7 @@
   val conjecture_prefix : string
   val boolify_base : string
   val explicit_app_base : string
+  val type_pred_base : string
   val is_type_system_sound : type_system -> bool
   val type_system_types_dangerous_types : type_system -> bool
   val num_atp_type_args : theory -> type_system -> string -> int
@@ -514,8 +515,8 @@
   | _ => raise Fail "expected two-argument type constructor"
 
 fun type_pred_combatom type_sys ty tm =
-  CombApp (CombConst ((const_prefix ^ type_pred_base, type_pred_base),
-                      pred_combtyp ty, [ty]), tm)
+  CombApp (CombConst (`make_fixed_const type_pred_base, pred_combtyp ty, [ty]),
+           tm)
   |> repair_combterm_consts type_sys
   |> AAtom