--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Mar 04 22:05:01 2015 +0100
@@ -752,14 +752,14 @@
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
- val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_term x)] (map SOME [c,x,t])
+ val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
(if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
in rth end
| ("x+t",[t]) =>
let
- val T = Thm.ctyp_of_term x
+ val T = Thm.ctyp_of_cterm x
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
@@ -775,7 +775,7 @@
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
- val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_term x)] (map SOME [c,x])
+ val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
val rth = th
in rth end
@@ -786,7 +786,7 @@
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
- val T = Thm.ctyp_of_term x
+ val T = Thm.ctyp_of_cterm x
val cr = dest_frac c
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
val cz = Thm.dest_arg ct
@@ -803,14 +803,14 @@
in rth end
| ("x+t",[t]) =>
let
- val T = Thm.ctyp_of_term x
+ val T = Thm.ctyp_of_cterm x
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
in rth end
| ("c*x",[c]) =>
let
- val T = Thm.ctyp_of_term x
+ val T = Thm.ctyp_of_cterm x
val cr = dest_frac c
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
val cz = Thm.dest_arg ct
@@ -820,7 +820,7 @@
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
- val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_term x)] (map SOME [c,x])
+ val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
(if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
val rth = th
in rth end
@@ -830,7 +830,7 @@
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
- val T = Thm.ctyp_of_term x
+ val T = Thm.ctyp_of_cterm x
val cr = dest_frac c
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
@@ -845,14 +845,14 @@
in rth end
| ("x+t",[t]) =>
let
- val T = Thm.ctyp_of_term x
+ val T = Thm.ctyp_of_cterm x
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
in rth end
| ("c*x",[c]) =>
let
- val T = Thm.ctyp_of_term x
+ val T = Thm.ctyp_of_cterm x
val cr = dest_frac c
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
@@ -874,7 +874,7 @@
fun field_isolate_conv phi ctxt vs ct = case Thm.term_of ct of
Const(@{const_name Orderings.less},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
- val T = Thm.ctyp_of_term ca
+ val T = Thm.ctyp_of_cterm ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
@@ -883,7 +883,7 @@
in rth end
| Const(@{const_name Orderings.less_eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
- val T = Thm.ctyp_of_term ca
+ val T = Thm.ctyp_of_cterm ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
@@ -893,7 +893,7 @@
| Const(@{const_name HOL.eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
- val T = Thm.ctyp_of_term ca
+ val T = Thm.ctyp_of_cterm ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Mar 04 22:05:01 2015 +0100
@@ -80,7 +80,7 @@
Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
| _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
- val cT = Thm.ctyp_of_term x
+ val cT = Thm.ctyp_of_cterm x
val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
val nthx = Thm.abstract_rule xn x nth
val q = Thm.rhs_of nth
--- a/src/HOL/Decision_Procs/langford.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Wed Mar 04 22:05:01 2015 +0100
@@ -46,7 +46,7 @@
fun proveneF S =
let
val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
- val cT = Thm.ctyp_of_term a
+ val cT = Thm.ctyp_of_cterm a
val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
val f = prove_finite cT (dest_set S)
in (ne, f) end
@@ -231,7 +231,7 @@
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
let
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
- fun gen x t = Thm.apply (all (Thm.ctyp_of_term x)) (Thm.lambda x t)
+ fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
val p' = fold_rev gen ts p
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
--- a/src/HOL/HOL.thy Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/HOL.thy Wed Mar 04 22:05:01 2015 +0100
@@ -1223,7 +1223,7 @@
let
val n = case f of (Abs (x, _, _)) => x | _ => "x";
val cx = Thm.cterm_of thy x;
- val {T = xT, ...} = Thm.rep_cterm cx;
+ val xT = Thm.typ_of_cterm cx;
val cf = Thm.cterm_of thy f;
val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
val (_ $ _ $ g) = Thm.prop_of fx_g;
--- a/src/HOL/HOLCF/Cfun.thy Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Wed Mar 04 22:05:01 2015 +0100
@@ -144,7 +144,7 @@
let
val dest = Thm.dest_comb;
val f = (snd o dest o snd o dest) ct;
- val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_term f);
+ val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
val tr = instantiate' [SOME T, SOME U] [SOME f]
(mk_meta_eq @{thm Abs_cfun_inverse2});
val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
--- a/src/HOL/Import/import_rule.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Import/import_rule.ML Wed Mar 04 22:05:01 2015 +0100
@@ -54,7 +54,7 @@
fun meta_eq_to_obj_eq th =
let
val (tml, tmr) = Thm.dest_binop (strip_imp_concl (Thm.cprop_of th))
- val cty = Thm.ctyp_of_term tml
+ val cty = Thm.ctyp_of_cterm tml
val i = Drule.instantiate' [SOME cty] [SOME tml, SOME tmr]
@{thm meta_eq_to_obj_eq}
in
@@ -78,7 +78,7 @@
val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
val (cf, cg) = Thm.dest_binop t1c
val (cx, cy) = Thm.dest_binop t2c
- val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_term cf)
+ val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf)
val i1 = Drule.instantiate' [SOME fd, SOME fr]
[SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
val i2 = meta_mp i1 th1
@@ -92,7 +92,7 @@
val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
val (r, s) = Thm.dest_binop t1c
val (_, t) = Thm.dest_binop t2c
- val ty = Thm.ctyp_of_term r
+ val ty = Thm.ctyp_of_cterm r
val i1 = Drule.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
val i2 = meta_mp i1 th1
in
@@ -135,7 +135,7 @@
fun refl ctm =
let
- val cty = Thm.ctyp_of_term ctm
+ val cty = Thm.ctyp_of_cterm ctm
in
Drule.instantiate' [SOME cty] [SOME ctm] @{thm refl}
end
@@ -151,7 +151,7 @@
val th2 = trans (trans bl th1) br
val th3 = implies_elim_all th2
val th4 = Thm.forall_intr cv th3
- val i = Drule.instantiate' [SOME (Thm.ctyp_of_term cv), SOME (Thm.ctyp_of_term tl)]
+ val i = Drule.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
[SOME ll, SOME lr] @{thm ext2}
in
meta_mp i th4
@@ -203,7 +203,7 @@
val (th_s, abst) = Thm.dest_comb th_s
val rept = Thm.dest_arg th_s
val P = Thm.dest_arg cn
- val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_term rept)
+ val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
in
Drule.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
SOME (Thm.cterm_of thy (Free ("a", Thm.typ_of nty))),
@@ -212,7 +212,7 @@
fun tydef' tycname abs_name rep_name cP ct td_th thy =
let
- val ctT = Thm.ctyp_of_term ct
+ val ctT = Thm.ctyp_of_cterm ct
val nonempty = Drule.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
val th2 = meta_mp nonempty td_th
val c =
@@ -229,7 +229,7 @@
val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
val (th_s, abst) = Thm.dest_comb th_s
val rept = Thm.dest_arg th_s
- val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_term rept)
+ val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
val typedef_th =
Drule.instantiate'
[SOME nty, SOME oty]
--- a/src/HOL/Library/Code_Abstract_Nat.thy Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Wed Mar 04 22:05:01 2015 +0100
@@ -79,7 +79,7 @@
Thm.implies_elim
(Conv.fconv_rule (Thm.beta_conversion true)
(Drule.instantiate'
- [SOME (Thm.ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
+ [SOME (Thm.ctyp_of_cterm ct)] [SOME (Thm.lambda cv ct),
SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
Suc_if_eq)) (Thm.forall_intr cv' thm)
in
--- a/src/HOL/Library/Old_SMT/old_smt_real.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_real.ML Wed Mar 04 22:05:01 2015 +0100
@@ -97,7 +97,7 @@
mk_builtin_typ = z3_mk_builtin_typ,
mk_builtin_num = z3_mk_builtin_num,
mk_builtin_fun = (fn _ => fn sym => fn cts =>
- (case try (#T o Thm.rep_cterm o hd) cts of
+ (case try (Thm.typ_of_cterm o hd) cts of
SOME @{typ real} => z3_mk_builtin_fun sym cts
| _ => NONE)) }
--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML Wed Mar 04 22:05:01 2015 +0100
@@ -40,7 +40,6 @@
(*certified terms*)
val certify: Proof.context -> term -> cterm
- val typ_of: cterm -> typ
val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
@@ -149,22 +148,20 @@
fun mk_const_pat thy name destT =
let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
- in (destT (Thm.ctyp_of_term cpat), cpat) end
+ in (destT (Thm.ctyp_of_cterm cpat), cpat) end
val destT1 = hd o Thm.dest_ctyp
val destT2 = hd o tl o Thm.dest_ctyp
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun instT' ct = instT (Thm.ctyp_of_term ct)
+fun instT' ct = instT (Thm.ctyp_of_cterm ct)
(* certified terms *)
fun certify ctxt = Proof_Context.cterm_of ctxt
-fun typ_of ct = #T (Thm.rep_cterm ct)
-
fun dest_cabs ct ctxt =
(case Thm.term_of ct of
Abs _ =>
--- a/src/HOL/Library/Old_SMT/old_z3_interface.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML Wed Mar 04 22:05:01 2015 +0100
@@ -170,7 +170,7 @@
fun mk_distinct [] = mk_true
| mk_distinct (cts as (ct :: _)) =
Thm.apply (Old_SMT_Utils.instT' ct distinct)
- (mk_list (Thm.ctyp_of_term ct) cts)
+ (mk_list (Thm.ctyp_of_cterm ct) cts)
val access =
Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} Old_SMT_Utils.destT1
@@ -179,7 +179,7 @@
val update = Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd}
(Thm.dest_ctyp o Old_SMT_Utils.destT1)
fun mk_update array index value =
- let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
+ let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
in
Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value
end
@@ -212,7 +212,7 @@
| (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
| (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
| _ =>
- (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
+ (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of
(Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
| (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
| (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Wed Mar 04 22:05:01 2015 +0100
@@ -50,14 +50,14 @@
fun mk_inv_of ctxt ct =
let
- val (dT, rT) = Term.dest_funT (Old_SMT_Utils.typ_of ct)
+ val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
val inv = Old_SMT_Utils.certify ctxt (mk_inv_into dT rT)
val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
in Thm.mk_binop inv univ ct end
fun mk_inj_prop ctxt ct =
let
- val (dT, rT) = Term.dest_funT (Old_SMT_Utils.typ_of ct)
+ val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
val inj = Old_SMT_Utils.certify ctxt (mk_inj_on dT rT)
val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Wed Mar 04 22:05:01 2015 +0100
@@ -104,14 +104,12 @@
use fast inference kernel rules during proof reconstruction.
*)
-val maxidx_of = #maxidx o Thm.rep_cterm
-
fun mk_inst ctxt vars =
let
val max = fold (Integer.max o fst) vars 0
val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
fun mk (i, v) =
- (v, Old_SMT_Utils.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
+ (v, Old_SMT_Utils.certify ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
in map mk vars end
fun close ctxt (ct, vars) =
@@ -131,7 +129,7 @@
val cv =
(case AList.lookup (op =) vars 0 of
SOME cv => cv
- | _ => Old_SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
+ | _ => Old_SMT_Utils.certify ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T)))
fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
val vars' = map_filter dec vars
in (Thm.apply (Old_SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
@@ -150,7 +148,7 @@
local
fun prep (ct, vars) (maxidx, all_vars) =
let
- val maxidx' = maxidx + maxidx_of ct + 1
+ val maxidx' = maxidx + Thm.maxidx_of_cterm ct + 1
fun part (i, cv) =
(case AList.lookup (op =) all_vars i of
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Wed Mar 04 22:05:01 2015 +0100
@@ -157,7 +157,7 @@
let
val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
val cv = Old_SMT_Utils.certify ctxt'
- (Free (n, map Old_SMT_Utils.typ_of cvs' ---> Old_SMT_Utils.typ_of ct))
+ (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct))
val cu = Drule.list_comb (cv, cvs')
val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
val beta_norm' = beta_norm orelse not (null cvs')
--- a/src/HOL/Library/positivstellensatz.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Wed Mar 04 22:05:01 2015 +0100
@@ -515,20 +515,20 @@
fun mk_forall x th =
Drule.arg_cong_rule
- (instantiate_cterm' [SOME (Thm.ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" })
+ (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
(Thm.abstract_rule (name_of x) x th)
val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
- fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_term v)) (Thm.lambda v t)
+ fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
fun choose v th th' =
case Thm.concl_of th of
@{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
- val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_term) p
+ val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
val th0 = fconv_rule (Thm.beta_conversion true)
(instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
val pv = (Thm.rhs_of o Thm.beta_conversion true)
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Wed Mar 04 22:05:01 2015 +0100
@@ -378,7 +378,8 @@
fun rewrite computer ct =
let
val thy = Thm.theory_of_cterm ct
- val {t=t',T=ty,...} = Thm.rep_cterm ct
+ val t' = Thm.term_of ct
+ val ty = Thm.typ_of_cterm ct
val _ = super_theory (theory_of computer) thy
val naming = naming_of computer
val (encoding, t) = remove_types (encoding_of computer) t'
@@ -507,7 +508,7 @@
fun compute_inst (s, ct) vs =
let
val _ = super_theory (Thm.theory_of_cterm ct) thy
- val ty = Thm.typ_of (Thm.ctyp_of_term ct)
+ val ty = Thm.typ_of_cterm ct
in
(case Symtab.lookup vartab s of
NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
--- a/src/HOL/Multivariate_Analysis/normarith.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Wed Mar 04 22:05:01 2015 +0100
@@ -258,7 +258,7 @@
local
val pth_zero = @{thm norm_zero}
- val tv_n = (Thm.ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
+ val tv_n = (Thm.ctyp_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
pth_zero
val concl = Thm.dest_arg o Thm.cprop_of
fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
@@ -319,7 +319,7 @@
(fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
in fst (RealArith.real_linear_prover translator
- (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_term t)],[]) pth_zero)
+ (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_cterm t)],[]) pth_zero)
zerodests,
map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
@@ -342,8 +342,8 @@
val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
- fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
- fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
+ fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
+ fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Proof_Context.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns
val replace_conv = try_conv (rewrs_conv asl)
val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 04 22:05:01 2015 +0100
@@ -14,7 +14,7 @@
let
val thy = Thm.theory_of_thm st;
val cgoal = nth (cprems_of st) (i - 1);
- val {maxidx, ...} = Thm.rep_cterm cgoal;
+ val maxidx = Thm.maxidx_of_cterm cgoal;
val j = maxidx + 1;
val tyinst' = map (apfst (Logic.incr_tvar j)) tyinst;
val ps = Logic.strip_params (Thm.term_of cgoal);
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Mar 04 22:05:01 2015 +0100
@@ -485,7 +485,7 @@
val (cf, ct) =
Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th));
val arg_cong' = Drule.instantiate'
- [SOME (Thm.ctyp_of_term ct)]
+ [SOME (Thm.ctyp_of_cterm ct)]
[NONE, SOME ct, SOME cf] (arg_cong RS iffD2);
val inst = Thm.first_order_match (ct,
Thm.dest_arg (Thm.dest_arg (Thm.cprop_of th')))
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Wed Mar 04 22:05:01 2015 +0100
@@ -433,11 +433,11 @@
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
-val ct1' = Thm.cterm_of @{theory} (term_of_dB [] (#T (Thm.rep_cterm ct1)) dB1);
+val ct1' = Thm.cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
-val ct2' = Thm.cterm_of @{theory} (term_of_dB [] (#T (Thm.rep_cterm ct2)) dB2);
+val ct2' = Thm.cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
*}
end
--- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Mar 04 22:05:01 2015 +0100
@@ -133,8 +133,7 @@
fun mtch (env as (tyinsts, insts)) =
fn (Var (ixn, T), ct) =>
(case AList.lookup (op =) insts ixn of
- NONE =>
- (naive_typ_match (T, Thm.typ_of (Thm.ctyp_of_term ct)) tyinsts, (ixn, ct) :: insts)
+ NONE => (naive_typ_match (T, Thm.typ_of_cterm ct) tyinsts, (ixn, ct) :: insts)
| SOME _ => env)
| (f $ t, ct) =>
let val (cf, ct') = Thm.dest_comb ct;
@@ -154,7 +153,7 @@
(Thm.ctyp_of thy (TVar (v, S)), Thm.ctyp_of thy U)) tyinsts;
val insts' =
map (fn (idxn, ct) =>
- (Thm.cterm_of thy (Var (idxn, Thm.typ_of (Thm.ctyp_of_term ct))), ct)) insts;
+ (Thm.cterm_of thy (Var (idxn, Thm.typ_of_cterm ct)), ct)) insts;
val rule' = Thm.instantiate (tyinsts', insts') rule;
in fold Thm.elim_implies prems rule' end;
@@ -216,19 +215,19 @@
fun in_set ps tree =
let
val (_, [l, x, _, r]) = Drule.strip_comb tree;
- val xT = Thm.ctyp_of_term x;
+ val xT = Thm.ctyp_of_cterm x;
in
(case ps of
[] =>
instantiate
- [(Thm.ctyp_of_term x_in_set_root, xT)]
+ [(Thm.ctyp_of_cterm x_in_set_root, xT)]
[(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root}
| Left :: ps' =>
let
val in_set_l = in_set ps' l;
val in_set_left' =
instantiate
- [(Thm.ctyp_of_term x_in_set_left, xT)]
+ [(Thm.ctyp_of_cterm x_in_set_left, xT)]
[(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left};
in discharge [in_set_l] in_set_left' end
| Right :: ps' =>
@@ -236,7 +235,7 @@
val in_set_r = in_set ps' r;
val in_set_right' =
instantiate
- [(Thm.ctyp_of_term x_in_set_right, xT)]
+ [(Thm.ctyp_of_cterm x_in_set_right, xT)]
[(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right};
in discharge [in_set_r] in_set_right' end)
end;
@@ -288,7 +287,7 @@
val ct =
@{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
|> Thm.dest_comb |> #2;
- val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+ val [alpha] = ct |> Thm.ctyp_of_cterm |> Thm.dest_ctyp;
in (alpha, #1 (dest_Var (Thm.term_of ct))) end;
in
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed Mar 04 22:05:01 2015 +0100
@@ -713,8 +713,7 @@
(i_opt : int option) : thm -> 'a list = fn st =>
let
val t_raws =
- Thm.rep_thm st
- |> #prop
+ Thm.prop_of st
|> strip_top_all_vars []
|> snd
|> Logic.strip_horn
--- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Mar 04 22:05:01 2015 +0100
@@ -128,9 +128,9 @@
val thy = Proof_Context.theory_of ctxt
fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
- val typ = (Thm.typ_of o Thm.ctyp_of_term) rel
+ val typ = Thm.typ_of_cterm rel
val POS_const = Thm.cterm_of thy (mk_POS typ)
- val var = Thm.cterm_of thy (Var (("X", #maxidx (Thm.rep_cterm (rel)) + 1), typ))
+ val var = Thm.cterm_of thy (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
val goal =
Thm.apply (Thm.cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
in
@@ -513,7 +513,7 @@
fun cconl_of thm = Drule.strip_imp_concl (Thm.cprop_of thm)
fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
- val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+ val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
val lhs = lhs_of rule1;
val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
val rule3 =
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Mar 04 22:05:01 2015 +0100
@@ -408,7 +408,7 @@
val ct =
thm |> Thm.cprop_of |> Drule.strip_imp_concl
|> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
- val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
+ val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def
val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
in
--- a/src/HOL/Tools/Lifting/lifting_term.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Wed Mar 04 22:05:01 2015 +0100
@@ -440,7 +440,7 @@
fun rewr_imp rule ct =
let
- val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+ val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
val lhs_rule = get_lhs rule1;
val rule2 = Thm.rename_boundvars (Thm.term_of lhs_rule) (Thm.term_of ct) rule1;
val lhs_ct = Thm.dest_fun ct
--- a/src/HOL/Tools/Meson/meson.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Wed Mar 04 22:05:01 2015 +0100
@@ -347,7 +347,7 @@
assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
local
val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
- val spec_varT = #T (Thm.rep_cterm spec_var);
+ val spec_varT = Thm.typ_of_cterm spec_var;
fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
in
fun freeze_spec th ctxt =
--- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Wed Mar 04 22:05:01 2015 +0100
@@ -103,7 +103,7 @@
let
val thy = Thm.theory_of_cterm ct
val Abs(x,_,body) = Thm.term_of ct
- val Type(@{type_name fun}, [xT,bodyT]) = Thm.typ_of (Thm.ctyp_of_term ct)
+ val Type (@{type_name fun}, [xT,bodyT]) = Thm.typ_of_cterm ct
val cxT = Thm.ctyp_of thy xT
val cbodyT = Thm.ctyp_of thy bodyT
fun makeK () =
--- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Wed Mar 04 22:05:01 2015 +0100
@@ -49,7 +49,7 @@
Const (@{const_name HOL.eq}, _) $ _ $ t =>
let
val ct = Thm.cterm_of thy t
- val cT = Thm.ctyp_of_term ct
+ val cT = Thm.ctyp_of_cterm ct
in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
| Const (@{const_name disj}, _) $ t1 $ t2 =>
(if can HOLogic.dest_not t1 then t2 else t1)
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Mar 04 22:05:01 2015 +0100
@@ -760,7 +760,7 @@
| _ => is_number t orelse can HOLogic.dest_nat t
fun ty cts t =
- if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of (Thm.ctyp_of_term t)))
+ if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t))
then false
else case Thm.term_of t of
c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
@@ -800,7 +800,7 @@
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
let
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
- fun gen x t = Thm.apply (all (Thm.ctyp_of_term x)) (Thm.lambda x t)
+ fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
val p' = fold_rev gen ts p
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Mar 04 22:05:01 2015 +0100
@@ -73,7 +73,7 @@
val lhs = eq |> Thm.dest_arg1;
val pt_random_aux = lhs |> Thm.dest_fun;
val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
-val aT = pt_random_aux |> Thm.ctyp_of_term |> dest_ctyp_nth 1;
+val aT = pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1;
val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one},
@{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}];
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Mar 04 22:05:01 2015 +0100
@@ -541,7 +541,7 @@
(* Tactic for Generalising Free Variables in a Goal *)
fun inst_spec ctrm =
- Drule.instantiate' [SOME (Thm.ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
+ Drule.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
fun inst_spec_tac ctrms =
EVERY' (map (dtac o inst_spec) ctrms)
--- a/src/HOL/Tools/SMT/smt_real.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed Mar 04 22:05:01 2015 +0100
@@ -89,7 +89,7 @@
mk_builtin_typ = z3_mk_builtin_typ,
mk_builtin_num = z3_mk_builtin_num,
mk_builtin_fun = (fn _ => fn sym => fn cts =>
- (case try (#T o Thm.rep_cterm o hd) cts of
+ (case try (Thm.typ_of_cterm o hd) cts of
SOME @{typ real} => z3_mk_builtin_fun sym cts
| _ => NONE)) }
--- a/src/HOL/Tools/SMT/smt_util.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Wed Mar 04 22:05:01 2015 +0100
@@ -45,7 +45,6 @@
val instT': cterm -> ctyp * cterm -> cterm
(*certified terms*)
- val typ_of: cterm -> typ
val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
@@ -167,20 +166,18 @@
fun mk_const_pat thy name destT =
let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
- in (destT (Thm.ctyp_of_term cpat), cpat) end
+ in (destT (Thm.ctyp_of_cterm cpat), cpat) end
val destT1 = hd o Thm.dest_ctyp
val destT2 = hd o tl o Thm.dest_ctyp
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun instT' ct = instT (Thm.ctyp_of_term ct)
+fun instT' ct = instT (Thm.ctyp_of_cterm ct)
(* certified terms *)
-fun typ_of ct = #T (Thm.rep_cterm ct)
-
fun dest_cabs ct ctxt =
(case Thm.term_of ct of
Abs _ =>
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Mar 04 22:05:01 2015 +0100
@@ -136,7 +136,7 @@
val update =
SMT_Util.mk_const_pat @{theory} @{const_name fun_upd} (Thm.dest_ctyp o SMT_Util.destT1)
fun mk_update array index value =
- let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
+ let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
@@ -166,7 +166,7 @@
| (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
| (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
| _ =>
- (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
+ (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of
(Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
| (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
| (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
--- a/src/HOL/Tools/TFL/dcterm.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/TFL/dcterm.ML Wed Mar 04 22:05:01 2015 +0100
@@ -70,7 +70,7 @@
val mk_hol_const = Thm.cterm_of @{theory HOL} o Const;
fun mk_exists (r as (Bvar, Body)) =
- let val ty = #T(Thm.rep_cterm Bvar)
+ let val ty = Thm.typ_of_cterm Bvar
val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
in capply c (uncurry cabs r) end;
@@ -88,12 +88,12 @@
* The primitives.
*---------------------------------------------------------------------------*)
fun dest_const ctm =
- (case #t(Thm.rep_cterm ctm)
+ (case Thm.term_of ctm
of Const(s,ty) => {Name = s, Ty = ty}
| _ => raise ERR "dest_const" "not a constant");
fun dest_var ctm =
- (case #t(Thm.rep_cterm ctm)
+ (case Thm.term_of ctm
of Var((s,i),ty) => {Name=s, Ty=ty}
| Free(s,ty) => {Name=s, Ty=ty}
| _ => raise ERR "dest_var" "not a variable");
--- a/src/HOL/Tools/TFL/rules.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Wed Mar 04 22:05:01 2015 +0100
@@ -121,7 +121,7 @@
fun FILTER_DISCH_ALL P thm =
- let fun check tm = P (#t (Thm.rep_cterm tm))
+ let fun check tm = P (Thm.term_of tm)
in fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
end;
@@ -269,7 +269,7 @@
val gspec = Thm.forall_intr (Thm.cterm_of thy x) spec
in
fun SPEC tm thm =
- let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_term tm)], []) gspec
+ let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec
in thm RS (Thm.forall_elim tm gspec') end
end;
@@ -285,7 +285,7 @@
fun cty_theta s = map (fn (i, (S, ty)) => (Thm.ctyp_of s (TVar (i, S)), Thm.ctyp_of s ty))
fun ctm_theta s = map (fn (i, (_, tm2)) =>
let val ctm2 = Thm.cterm_of s tm2
- in (Thm.cterm_of s (Var(i,#T(Thm.rep_cterm ctm2))), ctm2)
+ in (Thm.cterm_of s (Var(i, Thm.typ_of_cterm ctm2)), ctm2)
end)
fun certify s (ty_theta,tm_theta) =
(cty_theta s (Vartab.dest ty_theta),
--- a/src/HOL/Tools/Transfer/transfer.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed Mar 04 22:05:01 2015 +0100
@@ -195,7 +195,7 @@
| _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
fun Rel_conv ct =
- let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
+ let val (cT, cT') = dest_funcT (Thm.ctyp_of_cterm ct)
val (cU, _) = dest_funcT cT'
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
@@ -441,8 +441,8 @@
val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
- val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_term r1))
- val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_term r2))
+ val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
+ val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
--- a/src/HOL/Tools/choice_specification.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/choice_specification.ML Wed Mar 04 22:05:01 2015 +0100
@@ -137,7 +137,7 @@
fun inst_all thy v thm =
let
val cv = Thm.cterm_of thy v
- val cT = Thm.ctyp_of_term cv
+ val cT = Thm.ctyp_of_cterm cv
val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
in thm RS spec' end
fun remove_alls frees thm = fold (inst_all (Thm.theory_of_thm thm)) frees thm
--- a/src/HOL/Tools/groebner.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/groebner.ML Wed Mar 04 22:05:01 2015 +0100
@@ -435,7 +435,7 @@
fun sym_conv eq =
let val (l,r) = Thm.dest_binop eq
- in instantiate' [SOME (Thm.ctyp_of_term l)] [SOME l, SOME r] eq_commute
+ in instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute
end;
(* FIXME : copied from cqe.ML -- complex QE*)
@@ -479,13 +479,13 @@
(* Conversion for the equivalence of existential statements where
EX quantifiers are rearranged differently *)
fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
- fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_term v)) (Thm.lambda v t)
+ fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
fun choose v th th' = case Thm.concl_of th of
@{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
- val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_term) p
+ val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
val th0 = Conv.fconv_rule (Thm.beta_conversion true)
(instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
val pv = (Thm.rhs_of o Thm.beta_conversion true)
@@ -504,7 +504,7 @@
val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
in Thm.implies_elim
(Conv.fconv_rule (Thm.beta_conversion true)
- (instantiate' [SOME (Thm.ctyp_of_term v)] [SOME p, SOME v] @{thm exI}))
+ (instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
th
end
fun ex_eq_conv t =
@@ -527,7 +527,7 @@
| Var ((s,_),_) => s
| _ => "x"
fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
- fun mk_exists v th = Drule.arg_cong_rule (ext (Thm.ctyp_of_term v))
+ fun mk_exists v th = Drule.arg_cong_rule (ext (Thm.ctyp_of_cterm v))
(Thm.abstract_rule (getname v) v th)
fun simp_ex_conv ctxt =
Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
@@ -739,7 +739,7 @@
let
fun mk_forall x p =
Thm.apply
- (Drule.cterm_rule (instantiate' [SOME (Thm.ctyp_of_term x)] [])
+ (Drule.cterm_rule (instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
@{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
val avs = Thm.add_cterm_frees tm []
val P' = fold mk_forall avs tm
@@ -919,7 +919,7 @@
| SOME (res as (theory, {is_const = _, dest_const,
mk_const, conv = ring_eq_conv})) =>
SOME (ring_and_ideal_conv theory
- dest_const (mk_const (Thm.ctyp_of_term tm)) (ring_eq_conv ctxt)
+ dest_const (mk_const (Thm.ctyp_of_cterm tm)) (ring_eq_conv ctxt)
(Semiring_Normalizer.semiring_normalize_wrapper ctxt res)))
fun presimplify ctxt add_thms del_thms =
@@ -945,7 +945,7 @@
Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
| _=> raise CTERM ("ideal_tac - lhs",[t])
fun exitac NONE = no_tac
- | exitac (SOME y) = rtac (instantiate' [SOME (Thm.ctyp_of_term y)] [NONE,SOME y] exI) 1
+ | exitac (SOME y) = rtac (instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI) 1
val claset = claset_of @{context}
in
--- a/src/HOL/Tools/int_arith.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/int_arith.ML Wed Mar 04 22:05:01 2015 +0100
@@ -25,7 +25,7 @@
val lhss0 = [@{cpat "0::?'a::ring"}];
fun proc0 phi ctxt ct =
- let val T = Thm.ctyp_of_term ct
+ let val T = Thm.ctyp_of_cterm ct
in if Thm.typ_of T = @{typ int} then NONE else
SOME (instantiate' [SOME T] [] zeroth)
end;
@@ -39,7 +39,7 @@
val lhss1 = [@{cpat "1::?'a::ring_1"}];
fun proc1 phi ctxt ct =
- let val T = Thm.ctyp_of_term ct
+ let val T = Thm.ctyp_of_cterm ct
in if Thm.typ_of T = @{typ int} then NONE else
SOME (instantiate' [SOME T] [] oneth)
end;
--- a/src/HOL/Tools/legacy_transfer.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/legacy_transfer.ML Wed Mar 04 22:05:01 2015 +0100
@@ -89,7 +89,7 @@
val tys = map snd (Term.add_vars t []);
val _ = if null tys then error "Transfer: unable to guess instance" else ();
val tyss = splits (curry Type.could_unify) tys;
- val get_ty = Thm.typ_of o Thm.ctyp_of_term o fst o direction_of;
+ val get_ty = Thm.typ_of_cterm o fst o direction_of;
val insts = map_filter (fn tys => get_first (fn (k, e) =>
if Type.could_unify (hd tys, range_type (get_ty k))
then SOME (direction_of k, transfer_rules_of e)
@@ -108,7 +108,7 @@
|> Variable.import true (map Drule.mk_term [raw_a, raw_D])
|>> map Drule.dest_term o snd;
val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
- val T = Thm.typ_of (Thm.ctyp_of_term a);
+ val T = Thm.typ_of_cterm a;
val (aT, bT) = (Term.range_type T, Term.domain_type T);
(* determine variables to transfer *)
--- a/src/HOL/Tools/numeral.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/numeral.ML Wed Mar 04 22:05:01 2015 +0100
@@ -38,16 +38,16 @@
local
val zero = @{cpat "0"};
-val zeroT = Thm.ctyp_of_term zero;
+val zeroT = Thm.ctyp_of_cterm zero;
val one = @{cpat "1"};
-val oneT = Thm.ctyp_of_term one;
+val oneT = Thm.ctyp_of_cterm one;
val numeral = @{cpat "numeral"};
-val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
+val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
val uminus = @{cpat "uminus"};
-val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus)));
+val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
--- a/src/HOL/Tools/numeral_simprocs.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Mar 04 22:05:01 2015 +0100
@@ -587,9 +587,9 @@
local
val zr = @{cpat "0"}
- val zT = Thm.ctyp_of_term zr
+ val zT = Thm.ctyp_of_cterm zr
val geq = @{cpat HOL.eq}
- val eqT = Thm.dest_ctyp (Thm.ctyp_of_term geq) |> hd
+ val eqT = Thm.dest_ctyp (Thm.ctyp_of_cterm geq) |> hd
val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
@@ -609,7 +609,7 @@
val ((x,y),(w,z)) =
(Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w]
- val T = Thm.ctyp_of_term x
+ val T = Thm.ctyp_of_cterm x
val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
@@ -619,7 +619,7 @@
fun proc2 phi ctxt ct =
let
val (l,r) = Thm.dest_binop ct
- val T = Thm.ctyp_of_term l
+ val T = Thm.ctyp_of_cterm l
in (case (Thm.term_of l, Thm.term_of r) of
(Const(@{const_name Fields.divide},_)$_$_, _) =>
let val (x,y) = Thm.dest_binop l val z = r
@@ -648,42 +648,42 @@
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
- val T = Thm.ctyp_of_term c
+ val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
- val T = Thm.ctyp_of_term c
+ val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
- val T = Thm.ctyp_of_term c
+ val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
- val T = Thm.ctyp_of_term c
+ val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
- val T = Thm.ctyp_of_term c
+ val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
- val T = Thm.ctyp_of_term c
+ val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
in SOME (mk_meta_eq th) end
| _ => NONE)
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Mar 04 22:05:01 2015 +0100
@@ -522,7 +522,7 @@
let
val cv = mth |> Thm.cprop_of |> Drule.strip_imp_concl
|> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg1
- val T = #T (Thm.rep_cterm cv)
+ val T = Thm.typ_of_cterm cv
in
mth
|> Thm.instantiate ([], [(cv, number_of T n)])
--- a/src/Pure/conv.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Pure/conv.ML Wed Mar 04 22:05:01 2015 +0100
@@ -158,7 +158,7 @@
fun rewr_conv rule ct =
let
- val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+ val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
val lhs = Thm.lhs_of rule1;
val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
val rule3 =
--- a/src/Pure/drule.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Pure/drule.ML Wed Mar 04 22:05:01 2015 +0100
@@ -649,7 +649,7 @@
val thy = Thm.theory_of_cterm ct;
val cert = Thm.cterm_of thy;
val certT = Thm.ctyp_of thy;
- val T = Thm.typ_of (Thm.ctyp_of_term ct);
+ val T = Thm.typ_of_cterm ct;
val a = certT (TVar (("'a", 0), []));
val x = cert (Var (("x", 0), T));
in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
--- a/src/Pure/more_thm.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Pure/more_thm.ML Wed Mar 04 22:05:01 2015 +0100
@@ -126,7 +126,7 @@
fun all_name (x, t) A =
let
val cert = Thm.cterm_of (Thm.theory_of_cterm t);
- val T = #T (Thm.rep_cterm t);
+ val T = Thm.typ_of_cterm t;
in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
fun all t A = all_name ("", t) A;
--- a/src/Pure/raw_simplifier.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Pure/raw_simplifier.ML Wed Mar 04 22:05:01 2015 +0100
@@ -1293,7 +1293,7 @@
val thy = Proof_Context.theory_of raw_ctxt;
val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
- val {maxidx, ...} = Thm.rep_cterm ct;
+ val maxidx = Thm.maxidx_of_cterm ct;
val _ =
Theory.subthy (Thm.theory_of_cterm ct, thy) orelse
raise CTERM ("rewrite_cterm: bad background theory", [ct]);
--- a/src/Pure/subgoal.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Pure/subgoal.ML Wed Mar 04 22:05:01 2015 +0100
@@ -70,7 +70,7 @@
val cert = Proof_Context.cterm_of ctxt;
val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
- val Ts = map (#T o Thm.rep_cterm) params;
+ val Ts = map Thm.typ_of_cterm params;
val ts = map Thm.term_of params;
val prop = Thm.full_prop_of th';
--- a/src/Pure/thm.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Pure/thm.ML Wed Mar 04 22:05:01 2015 +0100
@@ -33,7 +33,9 @@
val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
val theory_of_cterm: cterm -> theory
val term_of: cterm -> term
- val ctyp_of_term: cterm -> ctyp
+ val typ_of_cterm: cterm -> typ
+ val ctyp_of_cterm: cterm -> ctyp
+ val maxidx_of_cterm: cterm -> int
val cterm_of: theory -> term -> cterm
val dest_comb: cterm -> cterm * cterm
val dest_fun: cterm -> cterm
@@ -186,9 +188,13 @@
fun theory_of_cterm (Cterm {thy, ...}) = thy;
fun term_of (Cterm {t, ...}) = t;
-fun ctyp_of_term (Cterm {thy, T, maxidx, sorts, ...}) =
+fun typ_of_cterm (Cterm {T, ...}) = T;
+
+fun ctyp_of_cterm (Cterm {thy, T, maxidx, sorts, ...}) =
Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts};
+fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx;
+
fun cterm_of thy tm =
let
val (t, T, maxidx) = Sign.certify_term thy tm;
--- a/src/Tools/atomize_elim.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Tools/atomize_elim.ML Wed Mar 04 22:05:01 2015 +0100
@@ -117,7 +117,7 @@
if is_Bound thesis then all_tac
else let
val cthesis = Thm.cterm_of thy thesis
- val rule = instantiate' [SOME (Thm.ctyp_of_term cthesis)] [NONE, SOME cthesis]
+ val rule = instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
@{thm meta_spec}
in
compose_tac ctxt (false, rule, 1) i
--- a/src/Tools/induct.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Tools/induct.ML Wed Mar 04 22:05:01 2015 +0100
@@ -398,9 +398,9 @@
fun prep_var (x, SOME t) =
let
val cx = cert x;
- val xT = #T (Thm.rep_cterm cx);
+ val xT = Thm.typ_of_cterm cx;
val ct = cert (tune t);
- val tT = #T (Thm.rep_cterm ct);
+ val tT = Thm.typ_of_cterm ct;
in
if Type.could_unify (tT, xT) then SOME (cx, ct)
else error (Pretty.string_of (Pretty.block
@@ -576,7 +576,7 @@
val pairs = Vartab.dest (Envir.term_env env);
val types = Vartab.dest (Envir.type_env env);
val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
- val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
+ val xs = map2 (curry (cert o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
in
--- a/src/Tools/nbe.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Tools/nbe.ML Wed Mar 04 22:05:01 2015 +0100
@@ -581,7 +581,7 @@
fun mk_equals ctxt lhs raw_rhs =
let
val thy = Proof_Context.theory_of ctxt;
- val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
+ val ty = Thm.typ_of_cterm lhs;
val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
val rhs = Thm.cterm_of thy raw_rhs;
in Thm.mk_binop eq lhs rhs end;