src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42549 b9754f26c7bc
parent 42544 75cb06eee990
child 42551 cd99d6d3027a
--- 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)