src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42549 b9754f26c7bc
parent 42544 75cb06eee990
child 42551 cd99d6d3027a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -356,29 +356,33 @@
     1.4                list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
     1.5            end
     1.6          | SOME b =>
     1.7 -          if b = boolify_base then
     1.8 -            aux (SOME @{typ bool}) [] (hd us)
     1.9 -          else if b = explicit_app_base then
    1.10 -            aux opt_T (nth us 1 :: extra_us) (hd us)
    1.11 -          else
    1.12 -            let
    1.13 -              val (c, mangled_us) = b |> unmangled_const |>> invert_const
    1.14 -              val num_ty_args = num_atp_type_args thy type_sys c
    1.15 -              val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
    1.16 -              (* Extra args from "hAPP" come after any arguments given directly
    1.17 -                 to the constant. *)
    1.18 -              val term_ts = map (aux NONE []) term_us
    1.19 -              val extra_ts = map (aux NONE []) extra_us
    1.20 -              val T =
    1.21 -                case opt_T of
    1.22 -                  SOME T => map fastype_of term_ts ---> T
    1.23 -                | NONE =>
    1.24 -                  if num_type_args thy c = length type_us then
    1.25 -                    Sign.const_instance thy (c,
    1.26 -                        map (type_from_fo_term tfrees) type_us)
    1.27 -                  else
    1.28 -                    HOLogic.typeT
    1.29 -            in list_comb (Const (c, T), term_ts @ extra_ts) end
    1.30 +          let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
    1.31 +            if b = boolify_base then
    1.32 +              aux (SOME @{typ bool}) [] (hd us)
    1.33 +            else if b = explicit_app_base then
    1.34 +              aux opt_T (nth us 1 :: extra_us) (hd us)
    1.35 +            else if b = type_pred_base then
    1.36 +              @{const True}
    1.37 +            else
    1.38 +              let
    1.39 +                val num_ty_args = num_atp_type_args thy type_sys b
    1.40 +                val (type_us, term_us) =
    1.41 +                  chop num_ty_args us |>> append mangled_us
    1.42 +                (* Extra args from "hAPP" come after any arguments given
    1.43 +                   directly to the constant. *)
    1.44 +                val term_ts = map (aux NONE []) term_us
    1.45 +                val extra_ts = map (aux NONE []) extra_us
    1.46 +                val T =
    1.47 +                  case opt_T of
    1.48 +                    SOME T => map fastype_of term_ts ---> T
    1.49 +                  | NONE =>
    1.50 +                    if num_type_args thy b = length type_us then
    1.51 +                      Sign.const_instance thy
    1.52 +                          (b, map (type_from_fo_term tfrees) type_us)
    1.53 +                    else
    1.54 +                      HOLogic.typeT
    1.55 +              in list_comb (Const (b, T), term_ts @ extra_ts) end
    1.56 +          end
    1.57          | NONE => (* a free or schematic variable *)
    1.58            let
    1.59              val ts = map (aux NONE []) (us @ extra_us)