src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42589 9f7c48463645
parent 42587 4fbb1de05169
child 42593 f9d7f1331a00
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4    | using_labels ls =
     1.5      "using " ^ space_implode " " (map string_for_label ls) ^ " "
     1.6  fun metis_name type_sys =
     1.7 -  if level_of_type_sys type_sys = Unsound then "metis" else "metisFT"
     1.8 +  if is_type_sys_fairly_sound type_sys then "metisFT" else "metis"
     1.9  fun metis_call type_sys ss = command_call (metis_name type_sys) ss
    1.10  fun metis_command type_sys i n (ls, ss) =
    1.11    using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
    1.12 @@ -342,12 +342,7 @@
    1.13      fun aux opt_T extra_us u =
    1.14        case u of
    1.15          ATerm (a, us) =>
    1.16 -        if a = type_tag_name then
    1.17 -          case us of
    1.18 -            [typ_u, term_u] =>
    1.19 -            aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
    1.20 -          | _ => raise FO_TERM us
    1.21 -        else if String.isPrefix tff_type_prefix a then
    1.22 +        if String.isPrefix tff_type_prefix a then
    1.23            @{const True} (* ignore TFF type information *)
    1.24          else case strip_prefix_and_unascii const_prefix a of
    1.25            SOME "equal" =>
    1.26 @@ -360,7 +355,12 @@
    1.27            end
    1.28          | SOME b =>
    1.29            let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
    1.30 -            if b = predicator_base then
    1.31 +            if b = type_tag_name then
    1.32 +              case mangled_us @ us of
    1.33 +                [typ_u, term_u] =>
    1.34 +                aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
    1.35 +              | _ => raise FO_TERM us
    1.36 +            else if b = predicator_base then
    1.37                aux (SOME @{typ bool}) [] (hd us)
    1.38              else if b = explicit_app_base then
    1.39                aux opt_T (nth us 1 :: extra_us) (hd us)