src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42551 cd99d6d3027a
parent 42549 b9754f26c7bc
child 42554 f83036b85a3a
equal deleted inserted replaced
42550:3031d342d514 42551:cd99d6d3027a
   344         if a = type_tag_name then
   344         if a = type_tag_name then
   345           case us of
   345           case us of
   346             [typ_u, term_u] =>
   346             [typ_u, term_u] =>
   347             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   347             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   348           | _ => raise FO_TERM us
   348           | _ => raise FO_TERM us
       
   349         else if String.isPrefix type_prefix a then
       
   350           @{const True} (* ignore TFF type information *)
   349         else case strip_prefix_and_unascii const_prefix a of
   351         else case strip_prefix_and_unascii const_prefix a of
   350           SOME "equal" =>
   352           SOME "equal" =>
   351           let val ts = map (aux NONE []) us in
   353           let val ts = map (aux NONE []) us in
   352             if length ts = 2 andalso hd ts aconv List.last ts then
   354             if length ts = 2 andalso hd ts aconv List.last ts then
   353               (* Vampire is keen on producing these. *)
   355               (* Vampire is keen on producing these. *)
   360             if b = boolify_base then
   362             if b = boolify_base then
   361               aux (SOME @{typ bool}) [] (hd us)
   363               aux (SOME @{typ bool}) [] (hd us)
   362             else if b = explicit_app_base then
   364             else if b = explicit_app_base then
   363               aux opt_T (nth us 1 :: extra_us) (hd us)
   365               aux opt_T (nth us 1 :: extra_us) (hd us)
   364             else if b = type_pred_base then
   366             else if b = type_pred_base then
   365               @{const True}
   367               @{const True} (* ignore type predicates *)
   366             else
   368             else
   367               let
   369               let
   368                 val num_ty_args = num_atp_type_args thy type_sys b
   370                 val num_ty_args = num_atp_type_args thy type_sys b
   369                 val (type_us, term_us) =
   371                 val (type_us, term_us) =
   370                   chop num_ty_args us |>> append mangled_us
   372                   chop num_ty_args us |>> append mangled_us