src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42227 662b50b7126f
parent 42180 a6c141925a8a
child 42361 23f352990944
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon Apr 04 16:35:46 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon Apr 04 18:53:35 2011 +0200
     1.3 @@ -345,23 +345,23 @@
     1.4            end
     1.5          | SOME b =>
     1.6            let
     1.7 -            val c = invert_const b
     1.8 +            val (c, mangled_us) = b |> unmangled_const |>> invert_const
     1.9              val num_ty_args = num_atp_type_args thy type_sys c
    1.10 -            val (type_us, term_us) = chop num_ty_args us
    1.11 +            val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
    1.12              (* Extra args from "hAPP" come after any arguments given directly to
    1.13                 the constant. *)
    1.14              val term_ts = map (aux NONE []) term_us
    1.15              val extra_ts = map (aux NONE []) extra_us
    1.16 -            val t =
    1.17 -              Const (c, case opt_T of
    1.18 -                          SOME T => map fastype_of term_ts ---> T
    1.19 -                        | NONE =>
    1.20 -                          if num_type_args thy c = length type_us then
    1.21 -                            Sign.const_instance thy (c,
    1.22 -                                map (type_from_fo_term tfrees) type_us)
    1.23 -                          else
    1.24 -                            HOLogic.typeT)
    1.25 -          in list_comb (t, term_ts @ extra_ts) end
    1.26 +            val T =
    1.27 +              case opt_T of
    1.28 +                SOME T => map fastype_of term_ts ---> T
    1.29 +              | NONE =>
    1.30 +                if num_type_args thy c = length type_us then
    1.31 +                  Sign.const_instance thy (c,
    1.32 +                      map (type_from_fo_term tfrees) type_us)
    1.33 +                else
    1.34 +                  HOLogic.typeT
    1.35 +          in list_comb (Const (c, T), term_ts @ extra_ts) end
    1.36          | NONE => (* a free or schematic variable *)
    1.37            let
    1.38              val ts = map (aux NONE []) (us @ extra_us)
    1.39 @@ -399,7 +399,8 @@
    1.40    | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
    1.41    | uncombine_term (t as Const (x as (s, _))) =
    1.42      (case AList.lookup (op =) combinator_table s of
    1.43 -       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
    1.44 +       SOME thm => thm |> prop_of |> specialize_type @{theory} x
    1.45 +                       |> Logic.dest_equals |> snd
    1.46       | NONE => t)
    1.47    | uncombine_term t = t
    1.48