--- a/src/HOL/Tools/SMT/smt_translate.ML Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Nov 22 15:45:43 2010 +0100
@@ -52,6 +52,9 @@
structure SMT_Translate: SMT_TRANSLATE =
struct
+structure U = SMT_Utils
+
+
(* intermediate term structure *)
datatype squant = SForall | SExists
@@ -107,13 +110,6 @@
(* utility functions *)
-val dest_funT =
- let
- fun dest Ts 0 T = (rev Ts, T)
- | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
- | dest _ _ T = raise TYPE ("dest_funT", [T], [])
- in dest [] end
-
val quantifier = (fn
@{const_name All} => SOME SForall
| @{const_name Ex} => SOME SExists
@@ -348,7 +344,7 @@
and new_dtyps dts cx =
let
fun new_decl i t =
- let val (Ts, T) = dest_funT i (Term.fastype_of t)
+ let val (Ts, T) = U.dest_funT i (Term.fastype_of t)
in
fold_map transT Ts ##>> transT T ##>>
new_fun func_prefix t NONE #>> swap
@@ -396,7 +392,7 @@
| _ => raise TERM ("smt_translate", [t]))
and transs t T ts =
- let val (Us, U) = dest_funT (length ts) T
+ let val (Us, U) = U.dest_funT (length ts) T
in
fold_map transT Us ##>> transT U #-> (fn Up =>
fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)