--- 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
--- 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
--- 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)
--- 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]}
--- 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)
--- 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')))
--- 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
--- 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;
--- 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)
--- 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 _ = [];
--- 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