reconstruct TFF type predicates correctly for ToFoF
authorblanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 42551cd99d6d3027a
parent 42550 3031d342d514
child 42552 e155be7125ba
reconstruct TFF type predicates correctly for ToFoF
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     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
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     2.3 @@ -24,6 +24,7 @@
     2.4    val boolify_base : string
     2.5    val explicit_app_base : string
     2.6    val type_pred_base : string
     2.7 +  val type_prefix : string
     2.8    val is_type_system_sound : type_system -> bool
     2.9    val type_system_types_dangerous_types : type_system -> bool
    2.10    val num_atp_type_args : theory -> type_system -> string -> int