src/HOL/Tools/SMT/smt_translate.ML
changeset 40663 e080c9e68752
parent 40579 98ebd2300823
child 40664 e023788a91a1
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 15:45:42 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 15:45:43 2010 +0100
     1.3 @@ -52,6 +52,9 @@
     1.4  structure SMT_Translate: SMT_TRANSLATE =
     1.5  struct
     1.6  
     1.7 +structure U = SMT_Utils
     1.8 +
     1.9 +
    1.10  (* intermediate term structure *)
    1.11  
    1.12  datatype squant = SForall | SExists
    1.13 @@ -107,13 +110,6 @@
    1.14  
    1.15  (* utility functions *)
    1.16  
    1.17 -val dest_funT =
    1.18 -  let
    1.19 -    fun dest Ts 0 T = (rev Ts, T)
    1.20 -      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
    1.21 -      | dest _ _ T = raise TYPE ("dest_funT", [T], [])
    1.22 -  in dest [] end
    1.23 -
    1.24  val quantifier = (fn
    1.25      @{const_name All} => SOME SForall
    1.26    | @{const_name Ex} => SOME SExists
    1.27 @@ -348,7 +344,7 @@
    1.28      and new_dtyps dts cx =
    1.29        let
    1.30          fun new_decl i t =
    1.31 -          let val (Ts, T) = dest_funT i (Term.fastype_of t)
    1.32 +          let val (Ts, T) = U.dest_funT i (Term.fastype_of t)
    1.33            in
    1.34              fold_map transT Ts ##>> transT T ##>>
    1.35              new_fun func_prefix t NONE #>> swap
    1.36 @@ -396,7 +392,7 @@
    1.37        | _ => raise TERM ("smt_translate", [t]))
    1.38  
    1.39      and transs t T ts =
    1.40 -      let val (Us, U) = dest_funT (length ts) T
    1.41 +      let val (Us, U) = U.dest_funT (length ts) T
    1.42        in
    1.43          fold_map transT Us ##>> transT U #-> (fn Up =>
    1.44          fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)