src/HOL/Tools/SMT/smt_utils.ML

--- a/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -10,7 +10,6 @@
   val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
 
   (* types *)
-  val split_type: typ -> typ * typ
   val dest_funT: int -> typ -> typ list * typ
 
   (* terms *)
@@ -57,8 +56,6 @@
 
 (* types *)
 
-fun split_type T = (Term.domain_type T, Term.range_type T)
-
 val dest_funT =
   let
     fun dest Ts 0 T = (rev Ts, T)