src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 41138 eb80538166b6
parent 41136 30bedf58b177
child 41140 9c68004b8c9d
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
     1.3 @@ -311,7 +311,7 @@
     1.4          ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
     1.5        | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
     1.6        | ATerm (a, us) =>
     1.7 -        if a = type_wrapper_name then
     1.8 +        if a = type_tag_name then
     1.9            case us of
    1.10              [typ_u, term_u] =>
    1.11              aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u