src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42693 3c2baf9b3c61
parent 42691 6efda6167e5d
child 42694 30278eb9c9db
equal deleted inserted replaced
42692:60359df11dc4 42693:3c2baf9b3c61
   616 fun list_app head args = fold (curry (CombApp o swap)) args head
   616 fun list_app head args = fold (curry (CombApp o swap)) args head
   617 
   617 
   618 fun explicit_app arg head =
   618 fun explicit_app arg head =
   619   let
   619   let
   620     val head_T = combtyp_of head
   620     val head_T = combtyp_of head
   621     val (_, res_T) = dest_funT head_T
   621     val (arg_T, res_T) = dest_funT head_T
   622     val explicit_app =
   622     val explicit_app =
   623       CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
   623       CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
   624                  [res_T])
   624                  [arg_T, res_T])
   625   in list_app explicit_app [head, arg] end
   625   in list_app explicit_app [head, arg] end
   626 fun list_explicit_app head args = fold explicit_app args head
   626 fun list_explicit_app head args = fold explicit_app args head
   627 
   627 
   628 fun introduce_explicit_apps_in_combterm sym_tab =
   628 fun introduce_explicit_apps_in_combterm sym_tab =
   629   let
   629   let