# HG changeset patch
# User wenzelm
# Date 1291205348 -3600
# Node ID 2f97215e79bfb8aec316b14db8981befb1a868e3
# Parent  48e01d16dd176d29d40e50f3c869036e4fe1991d
just one Term.dest_funT;

diff -r 48e01d16dd17 -r 2f97215e79bf src/HOL/HOLCF/Tools/holcf_library.ML
--- a/src/HOL/HOLCF/Tools/holcf_library.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -83,7 +83,7 @@
 
 fun mk_cabs t =
   let val T = fastype_of t
-  in cabs_const (Term.domain_type T, Term.range_type T) $ t end
+  in cabs_const (Term.dest_funT T) $ t end
 
 (* builds the expression (% v1 v2 .. vn. rhs) *)
 fun lambdas [] rhs = rhs
diff -r 48e01d16dd17 -r 2f97215e79bf src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -415,9 +415,6 @@
 
 val mk_var = Free
 
-fun dom_rng (Type("fun",[dom,rng])) = (dom,rng)
-  | dom_rng _ = raise ERR "dom_rng" "Not a functional type"
-
 fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
 
 local
@@ -1481,7 +1478,7 @@
                         _ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y)
                       | _ => raise ERR "mk_COMB" "Second theorem not an equality"
         val fty = type_of f
-        val (fd,fr) = dom_rng fty
+        val (fd,fr) = Term.dest_funT fty
         val comb_thm' = Drule.instantiate'
                             [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)]
                             [SOME (cterm_of thy f),SOME (cterm_of thy g),
@@ -1789,7 +1786,7 @@
         val (f,g) = case concl_of th1 of
                         _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
                       | _ => raise ERR "mk_ABS" "Bad conclusion"
-        val (fd,fr) = dom_rng (type_of f)
+        val (fd,fr) = Term.dest_funT (type_of f)
         val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
         val th2 = Thm.forall_intr cv th1
         val th3 = th2 COMP abs_thm'
@@ -1835,7 +1832,7 @@
                 in
                     fold_rev (fn v => fn th =>
                               let
-                                  val cdom = fst (dom_rng (fst (dom_rng cty)))
+                                  val cdom = fst (Term.dest_funT (fst (Term.dest_funT cty)))
                                   val vty  = type_of v
                                   val newcty = inst_type cdom vty cty
                                   val cc = cterm_of thy (Const(cname,newcty))
@@ -1991,7 +1988,7 @@
                                fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body)
                                  | dest_eta_abs body =
                                    let
-                                       val (dT,rT) = dom_rng (type_of body)
+                                       val (dT,rT) = Term.dest_funT (type_of body)
                                    in
                                        ("x",dT,body $ Bound 0)
                                    end
diff -r 48e01d16dd17 -r 2f97215e79bf src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -87,9 +87,6 @@
     Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
   end;
 
-fun dest_funT (Type ("fun",[S, T])) = (S, T)
-  | dest_funT T = raise TYPE ("dest_funT", [T], [])
- 
 fun mk_fun_comp (t, u) =
   let
     val (_, B) = dest_funT (fastype_of t)
diff -r 48e01d16dd17 -r 2f97215e79bf src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -234,9 +234,6 @@
     (Abs a) => snd (Term.dest_abs a)
   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
 
-fun dest_fun_type (Type("fun", [T, S])) = (T, S)
-  | dest_fun_type _ = error "dest_fun_type"
-
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 
 (* We apply apply_rsp only in case if the type needs lifting.
@@ -296,7 +293,7 @@
     | SOME (rel $ _ $ (rep $ (abs $ _))) =>
         let
           val thy = ProofContext.theory_of ctxt;
-          val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+          val (ty_a, ty_b) = dest_funT (fastype_of abs);
           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
         in
           case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
@@ -483,8 +480,8 @@
     (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
       let
         val thy = ProofContext.theory_of ctxt
-        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
-        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+        val (ty_b, ty_a) = dest_funT (fastype_of r1)
+        val (ty_c, ty_d) = dest_funT (fastype_of a2)
         val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
diff -r 48e01d16dd17 -r 2f97215e79bf 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)
diff -r 48e01d16dd17 -r 2f97215e79bf src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -131,7 +131,7 @@
       end)
 
 and trans_array T a =
-  let val (dT, rT) = U.split_type T
+  let val (dT, rT) = Term.dest_funT T
   in
     (case a of
       Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
@@ -151,11 +151,11 @@
 
 fun mk_update ([], u) _ = u
   | mk_update ([t], u) f =
-      uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u
+      uncurry mk_fun_upd (Term.dest_funT (Term.fastype_of f)) $ f $ t $ u
   | mk_update (t :: ts, u) f =
       let
-        val (dT, rT) = U.split_type (Term.fastype_of f)
-        val (dT', rT') = U.split_type rT
+        val (dT, rT) = Term.dest_funT (Term.fastype_of f)
+        val (dT', rT') = Term.dest_funT rT
       in
         mk_fun_upd dT rT $ f $ t $
           mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
diff -r 48e01d16dd17 -r 2f97215e79bf src/HOL/Tools/SMT/z3_proof_methods.ML
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -36,14 +36,14 @@
 
 fun mk_inv_of ctxt ct =
   let
-    val (dT, rT) = U.split_type (U.typ_of ct)
+    val (dT, rT) = Term.dest_funT (U.typ_of ct)
     val inv = U.certify ctxt (mk_inv_into dT rT)
     val univ = U.certify ctxt (mk_univ dT)
   in Thm.mk_binop inv univ ct end
 
 fun mk_inj_prop ctxt ct =
   let
-    val (dT, rT) = U.split_type (U.typ_of ct)
+    val (dT, rT) = Term.dest_funT (U.typ_of ct)
     val inj = U.certify ctxt (mk_inj_on dT rT)
     val univ = U.certify ctxt (mk_univ dT)
   in U.mk_cprop (Thm.mk_binop inj ct univ) end
diff -r 48e01d16dd17 -r 2f97215e79bf src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Tools/record.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -1016,8 +1016,7 @@
 fun mk_comp f g =
   let
     val X = fastype_of g;
-    val A = domain_type X;
-    val B = range_type X;
+    val (A, B) = dest_funT X;
     val C = range_type (fastype_of f);
     val T = (B --> C) --> (A --> B) --> A --> C;
   in Const (@{const_name Fun.comp}, T) $ f $ g end;
diff -r 48e01d16dd17 -r 2f97215e79bf src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -18,9 +18,6 @@
 
 (** general term functions **)
 
-fun dest_funT (Type ("fun",[S, T])) = (S, T)
-  | dest_funT T = raise TYPE ("dest_funT", [T], [])
- 
 fun mk_fun_comp (t, u) =
   let
     val (_, B) = dest_funT (fastype_of t)
diff -r 48e01d16dd17 -r 2f97215e79bf src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/Pure/term.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -48,6 +48,7 @@
   val dest_comb: term -> term * term
   val domain_type: typ -> typ
   val range_type: typ -> typ
+  val dest_funT: typ -> typ * typ
   val binder_types: typ -> typ list
   val body_type: typ -> typ
   val strip_type: typ -> typ list * typ
@@ -286,6 +287,10 @@
 fun domain_type (Type("fun", [T,_])) = T
 and range_type  (Type("fun", [_,T])) = T;
 
+fun dest_funT (Type ("fun", [T, U])) = (T, U)
+  | dest_funT T = raise TYPE ("dest_funT", [T], []);
+
+
 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   | binder_types _   =  [];
diff -r 48e01d16dd17 -r 2f97215e79bf src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/Tools/subtyping.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -774,8 +774,8 @@
         Syntax.string_of_term ctxt t ^ ":\n" ^
         Syntax.string_of_typ ctxt (fastype_of t));
 
-    val (Type ("fun", [T1, T2])) = fastype_of t
-      handle Bind => err_coercion ();
+    val (T1, T2) = Term.dest_funT (fastype_of t)
+      handle TYPE _ => err_coercion ();
 
     val a =
       (case T1 of