src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42539 f6ba908b8b27
parent 42531 a462dbaa584f
child 42541 8938507b2054
     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 @@ -334,10 +334,12 @@
     1.4    let
     1.5      fun aux opt_T extra_us u =
     1.6        case u of
     1.7 -        ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
     1.8 -      | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
     1.9 -      | ATerm (a, us) =>
    1.10 -        if a = type_tag_name then
    1.11 +        ATerm (a, us) =>
    1.12 +        if a = boolify_name then
    1.13 +          aux (SOME @{typ bool}) [] (hd us)
    1.14 +        else if a = explicit_app_name then
    1.15 +          aux opt_T (nth us 1 :: extra_us) (hd us)
    1.16 +        else if a = type_tag_name then
    1.17            case us of
    1.18              [typ_u, term_u] =>
    1.19              aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u