src/HOL/Tools/SMT/smt_translate.ML
changeset 41195 f59491d56327
parent 41173 7c6178d45cc8
child 41196 d23af676f9f8
equal deleted inserted replaced
41192:8aace46ffecb 41195:f59491d56327
   200     let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
   200     let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
   201     in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
   201     in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
   202 
   202 
   203   fun expf t i T ts =
   203   fun expf t i T ts =
   204     let val Ts = U.dest_funT i T |> fst |> drop (length ts)
   204     let val Ts = U.dest_funT i T |> fst |> drop (length ts)
   205     in Term.list_comb (t, ts) |> fold_rev eta Ts end
   205     in
       
   206       Term.list_comb (t, ts)
       
   207       |> Term.incr_boundvars (length Ts)
       
   208       |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
       
   209       |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
       
   210     end
   206 
   211 
   207   fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
   212   fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
   208     | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
   213     | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
   209     | expand (q as Const (@{const_name All}, T)) = exp2 T q
   214     | expand (q as Const (@{const_name All}, T)) = exp2 T q
   210     | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
   215     | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a