src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42551 cd99d6d3027a
parent 42549 b9754f26c7bc
child 42554 f83036b85a3a
     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 @@ -346,6 +346,8 @@
     1.4              [typ_u, term_u] =>
     1.5              aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
     1.6            | _ => raise FO_TERM us
     1.7 +        else if String.isPrefix type_prefix a then
     1.8 +          @{const True} (* ignore TFF type information *)
     1.9          else case strip_prefix_and_unascii const_prefix a of
    1.10            SOME "equal" =>
    1.11            let val ts = map (aux NONE []) us in
    1.12 @@ -362,7 +364,7 @@
    1.13              else if b = explicit_app_base then
    1.14                aux opt_T (nth us 1 :: extra_us) (hd us)
    1.15              else if b = type_pred_base then
    1.16 -              @{const True}
    1.17 +              @{const True} (* ignore type predicates *)
    1.18              else
    1.19                let
    1.20                  val num_ty_args = num_atp_type_args thy type_sys b