src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42539 f6ba908b8b27
parent 42531 a462dbaa584f
child 42541 8938507b2054
equal deleted inserted replaced
42538:9e3e45636459 42539:f6ba908b8b27
   332    should allow them to be inferred. *)
   332    should allow them to be inferred. *)
   333 fun raw_term_from_pred thy type_sys tfrees =
   333 fun raw_term_from_pred thy type_sys tfrees =
   334   let
   334   let
   335     fun aux opt_T extra_us u =
   335     fun aux opt_T extra_us u =
   336       case u of
   336       case u of
   337         ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   337         ATerm (a, us) =>
   338       | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
   338         if a = boolify_name then
   339       | ATerm (a, us) =>
   339           aux (SOME @{typ bool}) [] (hd us)
   340         if a = type_tag_name then
   340         else if a = explicit_app_name then
       
   341           aux opt_T (nth us 1 :: extra_us) (hd us)
       
   342         else if a = type_tag_name then
   341           case us of
   343           case us of
   342             [typ_u, term_u] =>
   344             [typ_u, term_u] =>
   343             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   345             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   344           | _ => raise FO_TERM us
   346           | _ => raise FO_TERM us
   345         else case strip_prefix_and_unascii const_prefix a of
   347         else case strip_prefix_and_unascii const_prefix a of