clarified signature;
authorwenzelm
Wed Mar 04 22:05:01 2015 +0100 (2015-03-04)
changeset 59586ddf6deaadfe8
parent 59585 68a770a8a09f
child 59588 c6f3dbe466b6
child 59589 6020e3dec7b5
clarified signature;
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/HOL.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/Import/import_rule.ML
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Library/Old_SMT/old_smt_real.ML
src/HOL/Library/Old_SMT/old_smt_utils.ML
src/HOL/Library/Old_SMT/old_z3_interface.ML
src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
src/HOL/Library/Old_SMT/old_z3_proof_parser.ML
src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Matrix_LP/Compute_Oracle/compute.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Proofs/Lambda/WeakNorm.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_util.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/legacy_transfer.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/numeral_simprocs.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/conv.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
src/Pure/raw_simplifier.ML
src/Pure/subgoal.ML
src/Pure/thm.ML
src/Tools/atomize_elim.ML
src/Tools/induct.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -752,14 +752,14 @@
     1.4                    (if neg then Thm.apply (Thm.apply clt c) cz
     1.5                      else Thm.apply (Thm.apply clt cz) c))
     1.6          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
     1.7 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_term x)] (map SOME [c,x,t])
     1.8 +        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
     1.9               (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
    1.10          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.11                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.12        in rth end
    1.13      | ("x+t",[t]) =>
    1.14         let
    1.15 -        val T = Thm.ctyp_of_term x
    1.16 +        val T = Thm.ctyp_of_cterm x
    1.17          val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
    1.18          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.19                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.20 @@ -775,7 +775,7 @@
    1.21                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.22                      else Thm.apply (Thm.apply clt cz) c))
    1.23          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    1.24 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_term x)] (map SOME [c,x])
    1.25 +        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    1.26               (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
    1.27          val rth = th
    1.28        in rth end
    1.29 @@ -786,7 +786,7 @@
    1.30     (case whatis x (Thm.dest_arg1 ct) of
    1.31      ("c*x+t",[c,t]) =>
    1.32         let
    1.33 -        val T = Thm.ctyp_of_term x
    1.34 +        val T = Thm.ctyp_of_cterm x
    1.35          val cr = dest_frac c
    1.36          val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
    1.37          val cz = Thm.dest_arg ct
    1.38 @@ -803,14 +803,14 @@
    1.39        in rth end
    1.40      | ("x+t",[t]) =>
    1.41         let
    1.42 -        val T = Thm.ctyp_of_term x
    1.43 +        val T = Thm.ctyp_of_cterm x
    1.44          val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
    1.45          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.46                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.47         in  rth end
    1.48      | ("c*x",[c]) =>
    1.49         let
    1.50 -        val T = Thm.ctyp_of_term x
    1.51 +        val T = Thm.ctyp_of_cterm x
    1.52          val cr = dest_frac c
    1.53          val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
    1.54          val cz = Thm.dest_arg ct
    1.55 @@ -820,7 +820,7 @@
    1.56                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.57                      else Thm.apply (Thm.apply clt cz) c))
    1.58          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    1.59 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_term x)] (map SOME [c,x])
    1.60 +        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    1.61               (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
    1.62          val rth = th
    1.63        in rth end
    1.64 @@ -830,7 +830,7 @@
    1.65     (case whatis x (Thm.dest_arg1 ct) of
    1.66      ("c*x+t",[c,t]) =>
    1.67         let
    1.68 -        val T = Thm.ctyp_of_term x
    1.69 +        val T = Thm.ctyp_of_cterm x
    1.70          val cr = dest_frac c
    1.71          val ceq = Thm.dest_fun2 ct
    1.72          val cz = Thm.dest_arg ct
    1.73 @@ -845,14 +845,14 @@
    1.74        in rth end
    1.75      | ("x+t",[t]) =>
    1.76         let
    1.77 -        val T = Thm.ctyp_of_term x
    1.78 +        val T = Thm.ctyp_of_cterm x
    1.79          val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
    1.80          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.81                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.82         in  rth end
    1.83      | ("c*x",[c]) =>
    1.84         let
    1.85 -        val T = Thm.ctyp_of_term x
    1.86 +        val T = Thm.ctyp_of_cterm x
    1.87          val cr = dest_frac c
    1.88          val ceq = Thm.dest_fun2 ct
    1.89          val cz = Thm.dest_arg ct
    1.90 @@ -874,7 +874,7 @@
    1.91  fun field_isolate_conv phi ctxt vs ct = case Thm.term_of ct of
    1.92    Const(@{const_name Orderings.less},_)$a$b =>
    1.93     let val (ca,cb) = Thm.dest_binop ct
    1.94 -       val T = Thm.ctyp_of_term ca
    1.95 +       val T = Thm.ctyp_of_cterm ca
    1.96         val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
    1.97         val nth = Conv.fconv_rule
    1.98           (Conv.arg_conv (Conv.arg1_conv
    1.99 @@ -883,7 +883,7 @@
   1.100     in rth end
   1.101  | Const(@{const_name Orderings.less_eq},_)$a$b =>
   1.102     let val (ca,cb) = Thm.dest_binop ct
   1.103 -       val T = Thm.ctyp_of_term ca
   1.104 +       val T = Thm.ctyp_of_cterm ca
   1.105         val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
   1.106         val nth = Conv.fconv_rule
   1.107           (Conv.arg_conv (Conv.arg1_conv
   1.108 @@ -893,7 +893,7 @@
   1.109  
   1.110  | Const(@{const_name HOL.eq},_)$a$b =>
   1.111     let val (ca,cb) = Thm.dest_binop ct
   1.112 -       val T = Thm.ctyp_of_term ca
   1.113 +       val T = Thm.ctyp_of_cterm ca
   1.114         val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
   1.115         val nth = Conv.fconv_rule
   1.116           (Conv.arg_conv (Conv.arg1_conv
     2.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Mar 04 20:50:20 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Mar 04 22:05:01 2015 +0100
     2.3 @@ -80,7 +80,7 @@
     2.4                     Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
     2.5                          Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
     2.6                   | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
     2.7 -   val cT = Thm.ctyp_of_term x
     2.8 +   val cT = Thm.ctyp_of_cterm x
     2.9     val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
    2.10     val nthx = Thm.abstract_rule xn x nth
    2.11     val q = Thm.rhs_of nth
     3.1 --- a/src/HOL/Decision_Procs/langford.ML	Wed Mar 04 20:50:20 2015 +0100
     3.2 +++ b/src/HOL/Decision_Procs/langford.ML	Wed Mar 04 22:05:01 2015 +0100
     3.3 @@ -46,7 +46,7 @@
     3.4          fun proveneF S =
     3.5            let
     3.6              val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
     3.7 -            val cT = Thm.ctyp_of_term a
     3.8 +            val cT = Thm.ctyp_of_cterm a
     3.9              val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
    3.10              val f = prove_finite cT (dest_set S)
    3.11           in (ne, f) end
    3.12 @@ -231,7 +231,7 @@
    3.13  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    3.14    let
    3.15      fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
    3.16 -    fun gen x t = Thm.apply (all (Thm.ctyp_of_term x)) (Thm.lambda x t)
    3.17 +    fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
    3.18      val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
    3.19      val p' = fold_rev gen ts p
    3.20    in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
     4.1 --- a/src/HOL/HOL.thy	Wed Mar 04 20:50:20 2015 +0100
     4.2 +++ b/src/HOL/HOL.thy	Wed Mar 04 22:05:01 2015 +0100
     4.3 @@ -1223,7 +1223,7 @@
     4.4          let
     4.5            val n = case f of (Abs (x, _, _)) => x | _ => "x";
     4.6            val cx = Thm.cterm_of thy x;
     4.7 -          val {T = xT, ...} = Thm.rep_cterm cx;
     4.8 +          val xT = Thm.typ_of_cterm cx;
     4.9            val cf = Thm.cterm_of thy f;
    4.10            val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
    4.11            val (_ $ _ $ g) = Thm.prop_of fx_g;
     5.1 --- a/src/HOL/HOLCF/Cfun.thy	Wed Mar 04 20:50:20 2015 +0100
     5.2 +++ b/src/HOL/HOLCF/Cfun.thy	Wed Mar 04 22:05:01 2015 +0100
     5.3 @@ -144,7 +144,7 @@
     5.4      let
     5.5        val dest = Thm.dest_comb;
     5.6        val f = (snd o dest o snd o dest) ct;
     5.7 -      val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_term f);
     5.8 +      val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
     5.9        val tr = instantiate' [SOME T, SOME U] [SOME f]
    5.10            (mk_meta_eq @{thm Abs_cfun_inverse2});
    5.11        val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
     6.1 --- a/src/HOL/Import/import_rule.ML	Wed Mar 04 20:50:20 2015 +0100
     6.2 +++ b/src/HOL/Import/import_rule.ML	Wed Mar 04 22:05:01 2015 +0100
     6.3 @@ -54,7 +54,7 @@
     6.4  fun meta_eq_to_obj_eq th =
     6.5    let
     6.6      val (tml, tmr) = Thm.dest_binop (strip_imp_concl (Thm.cprop_of th))
     6.7 -    val cty = Thm.ctyp_of_term tml
     6.8 +    val cty = Thm.ctyp_of_cterm tml
     6.9      val i = Drule.instantiate' [SOME cty] [SOME tml, SOME tmr]
    6.10        @{thm meta_eq_to_obj_eq}
    6.11    in
    6.12 @@ -78,7 +78,7 @@
    6.13      val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
    6.14      val (cf, cg) = Thm.dest_binop t1c
    6.15      val (cx, cy) = Thm.dest_binop t2c
    6.16 -    val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_term cf)
    6.17 +    val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf)
    6.18      val i1 = Drule.instantiate' [SOME fd, SOME fr]
    6.19        [SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
    6.20      val i2 = meta_mp i1 th1
    6.21 @@ -92,7 +92,7 @@
    6.22      val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
    6.23      val (r, s) = Thm.dest_binop t1c
    6.24      val (_, t) = Thm.dest_binop t2c
    6.25 -    val ty = Thm.ctyp_of_term r
    6.26 +    val ty = Thm.ctyp_of_cterm r
    6.27      val i1 = Drule.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
    6.28      val i2 = meta_mp i1 th1
    6.29    in
    6.30 @@ -135,7 +135,7 @@
    6.31  
    6.32  fun refl ctm =
    6.33    let
    6.34 -    val cty = Thm.ctyp_of_term ctm
    6.35 +    val cty = Thm.ctyp_of_cterm ctm
    6.36    in
    6.37      Drule.instantiate' [SOME cty] [SOME ctm] @{thm refl}
    6.38    end
    6.39 @@ -151,7 +151,7 @@
    6.40      val th2 = trans (trans bl th1) br
    6.41      val th3 = implies_elim_all th2
    6.42      val th4 = Thm.forall_intr cv th3
    6.43 -    val i = Drule.instantiate' [SOME (Thm.ctyp_of_term cv), SOME (Thm.ctyp_of_term tl)]
    6.44 +    val i = Drule.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
    6.45        [SOME ll, SOME lr] @{thm ext2}
    6.46    in
    6.47      meta_mp i th4
    6.48 @@ -203,7 +203,7 @@
    6.49      val (th_s, abst) = Thm.dest_comb th_s
    6.50      val rept = Thm.dest_arg th_s
    6.51      val P = Thm.dest_arg cn
    6.52 -    val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_term rept)
    6.53 +    val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
    6.54    in
    6.55      Drule.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
    6.56        SOME (Thm.cterm_of thy (Free ("a", Thm.typ_of nty))),
    6.57 @@ -212,7 +212,7 @@
    6.58  
    6.59  fun tydef' tycname abs_name rep_name cP ct td_th thy =
    6.60    let
    6.61 -    val ctT = Thm.ctyp_of_term ct
    6.62 +    val ctT = Thm.ctyp_of_cterm ct
    6.63      val nonempty = Drule.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
    6.64      val th2 = meta_mp nonempty td_th
    6.65      val c =
    6.66 @@ -229,7 +229,7 @@
    6.67      val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
    6.68      val (th_s, abst) = Thm.dest_comb th_s
    6.69      val rept = Thm.dest_arg th_s
    6.70 -    val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_term rept)
    6.71 +    val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
    6.72      val typedef_th =
    6.73         Drule.instantiate'
    6.74            [SOME nty, SOME oty]
     7.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Mar 04 20:50:20 2015 +0100
     7.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Mar 04 22:05:01 2015 +0100
     7.3 @@ -79,7 +79,7 @@
     7.4            Thm.implies_elim
     7.5             (Conv.fconv_rule (Thm.beta_conversion true)
     7.6               (Drule.instantiate'
     7.7 -               [SOME (Thm.ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
     7.8 +               [SOME (Thm.ctyp_of_cterm ct)] [SOME (Thm.lambda cv ct),
     7.9                   SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
    7.10                 Suc_if_eq)) (Thm.forall_intr cv' thm)
    7.11        in
     8.1 --- a/src/HOL/Library/Old_SMT/old_smt_real.ML	Wed Mar 04 20:50:20 2015 +0100
     8.2 +++ b/src/HOL/Library/Old_SMT/old_smt_real.ML	Wed Mar 04 22:05:01 2015 +0100
     8.3 @@ -97,7 +97,7 @@
     8.4    mk_builtin_typ = z3_mk_builtin_typ,
     8.5    mk_builtin_num = z3_mk_builtin_num,
     8.6    mk_builtin_fun = (fn _ => fn sym => fn cts =>
     8.7 -    (case try (#T o Thm.rep_cterm o hd) cts of
     8.8 +    (case try (Thm.typ_of_cterm o hd) cts of
     8.9        SOME @{typ real} => z3_mk_builtin_fun sym cts
    8.10      | _ => NONE)) }
    8.11  
     9.1 --- a/src/HOL/Library/Old_SMT/old_smt_utils.ML	Wed Mar 04 20:50:20 2015 +0100
     9.2 +++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML	Wed Mar 04 22:05:01 2015 +0100
     9.3 @@ -40,7 +40,6 @@
     9.4  
     9.5    (*certified terms*)
     9.6    val certify: Proof.context -> term -> cterm
     9.7 -  val typ_of: cterm -> typ
     9.8    val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
     9.9    val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
    9.10    val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
    9.11 @@ -149,22 +148,20 @@
    9.12  
    9.13  fun mk_const_pat thy name destT =
    9.14    let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
    9.15 -  in (destT (Thm.ctyp_of_term cpat), cpat) end
    9.16 +  in (destT (Thm.ctyp_of_cterm cpat), cpat) end
    9.17  
    9.18  val destT1 = hd o Thm.dest_ctyp
    9.19  val destT2 = hd o tl o Thm.dest_ctyp
    9.20  
    9.21  fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
    9.22  fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
    9.23 -fun instT' ct = instT (Thm.ctyp_of_term ct)
    9.24 +fun instT' ct = instT (Thm.ctyp_of_cterm ct)
    9.25  
    9.26  
    9.27  (* certified terms *)
    9.28  
    9.29  fun certify ctxt = Proof_Context.cterm_of ctxt
    9.30  
    9.31 -fun typ_of ct = #T (Thm.rep_cterm ct) 
    9.32 -
    9.33  fun dest_cabs ct ctxt =
    9.34    (case Thm.term_of ct of
    9.35      Abs _ =>
    10.1 --- a/src/HOL/Library/Old_SMT/old_z3_interface.ML	Wed Mar 04 20:50:20 2015 +0100
    10.2 +++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML	Wed Mar 04 22:05:01 2015 +0100
    10.3 @@ -170,7 +170,7 @@
    10.4  fun mk_distinct [] = mk_true
    10.5    | mk_distinct (cts as (ct :: _)) =
    10.6        Thm.apply (Old_SMT_Utils.instT' ct distinct)
    10.7 -        (mk_list (Thm.ctyp_of_term ct) cts)
    10.8 +        (mk_list (Thm.ctyp_of_cterm ct) cts)
    10.9  
   10.10  val access =
   10.11    Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} Old_SMT_Utils.destT1
   10.12 @@ -179,7 +179,7 @@
   10.13  val update = Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd}
   10.14    (Thm.dest_ctyp o Old_SMT_Utils.destT1)
   10.15  fun mk_update array index value =
   10.16 -  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
   10.17 +  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
   10.18    in
   10.19      Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value
   10.20    end
   10.21 @@ -212,7 +212,7 @@
   10.22    | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
   10.23    | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
   10.24    | _ =>
   10.25 -    (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
   10.26 +    (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of
   10.27        (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
   10.28      | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
   10.29      | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
    11.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Wed Mar 04 20:50:20 2015 +0100
    11.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Wed Mar 04 22:05:01 2015 +0100
    11.3 @@ -50,14 +50,14 @@
    11.4  
    11.5  fun mk_inv_of ctxt ct =
    11.6    let
    11.7 -    val (dT, rT) = Term.dest_funT (Old_SMT_Utils.typ_of ct)
    11.8 +    val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
    11.9      val inv = Old_SMT_Utils.certify ctxt (mk_inv_into dT rT)
   11.10      val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
   11.11    in Thm.mk_binop inv univ ct end
   11.12  
   11.13  fun mk_inj_prop ctxt ct =
   11.14    let
   11.15 -    val (dT, rT) = Term.dest_funT (Old_SMT_Utils.typ_of ct)
   11.16 +    val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
   11.17      val inj = Old_SMT_Utils.certify ctxt (mk_inj_on dT rT)
   11.18      val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
   11.19    in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
    12.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Wed Mar 04 20:50:20 2015 +0100
    12.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Wed Mar 04 22:05:01 2015 +0100
    12.3 @@ -104,14 +104,12 @@
    12.4    use fast inference kernel rules during proof reconstruction.
    12.5  *)
    12.6  
    12.7 -val maxidx_of = #maxidx o Thm.rep_cterm
    12.8 -
    12.9  fun mk_inst ctxt vars =
   12.10    let
   12.11      val max = fold (Integer.max o fst) vars 0
   12.12      val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
   12.13      fun mk (i, v) =
   12.14 -      (v, Old_SMT_Utils.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
   12.15 +      (v, Old_SMT_Utils.certify ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
   12.16    in map mk vars end
   12.17  
   12.18  fun close ctxt (ct, vars) =
   12.19 @@ -131,7 +129,7 @@
   12.20        val cv =
   12.21          (case AList.lookup (op =) vars 0 of
   12.22            SOME cv => cv
   12.23 -        | _ => Old_SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
   12.24 +        | _ => Old_SMT_Utils.certify ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T)))
   12.25        fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
   12.26        val vars' = map_filter dec vars
   12.27      in (Thm.apply (Old_SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
   12.28 @@ -150,7 +148,7 @@
   12.29  local
   12.30    fun prep (ct, vars) (maxidx, all_vars) =
   12.31      let
   12.32 -      val maxidx' = maxidx + maxidx_of ct + 1
   12.33 +      val maxidx' = maxidx + Thm.maxidx_of_cterm ct + 1
   12.34  
   12.35        fun part (i, cv) =
   12.36          (case AList.lookup (op =) all_vars i of
    13.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Wed Mar 04 20:50:20 2015 +0100
    13.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Wed Mar 04 22:05:01 2015 +0100
    13.3 @@ -157,7 +157,7 @@
    13.4          let
    13.5            val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
    13.6            val cv = Old_SMT_Utils.certify ctxt'
    13.7 -            (Free (n, map Old_SMT_Utils.typ_of cvs' ---> Old_SMT_Utils.typ_of ct))
    13.8 +            (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct))
    13.9            val cu = Drule.list_comb (cv, cvs')
   13.10            val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
   13.11            val beta_norm' = beta_norm orelse not (null cvs')
    14.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Mar 04 20:50:20 2015 +0100
    14.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Mar 04 22:05:01 2015 +0100
    14.3 @@ -515,20 +515,20 @@
    14.4  
    14.5      fun mk_forall x th =
    14.6        Drule.arg_cong_rule
    14.7 -        (instantiate_cterm' [SOME (Thm.ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" })
    14.8 +        (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
    14.9          (Thm.abstract_rule (name_of x) x th)
   14.10  
   14.11      val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   14.12  
   14.13      fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   14.14 -    fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_term v)) (Thm.lambda v t)
   14.15 +    fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
   14.16  
   14.17      fun choose v th th' =
   14.18        case Thm.concl_of th of
   14.19          @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
   14.20          let
   14.21            val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
   14.22 -          val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_term) p
   14.23 +          val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
   14.24            val th0 = fconv_rule (Thm.beta_conversion true)
   14.25              (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   14.26            val pv = (Thm.rhs_of o Thm.beta_conversion true)
    15.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Wed Mar 04 20:50:20 2015 +0100
    15.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Wed Mar 04 22:05:01 2015 +0100
    15.3 @@ -378,7 +378,8 @@
    15.4  fun rewrite computer ct =
    15.5      let
    15.6          val thy = Thm.theory_of_cterm ct
    15.7 -        val {t=t',T=ty,...} = Thm.rep_cterm ct
    15.8 +        val t' = Thm.term_of ct
    15.9 +        val ty = Thm.typ_of_cterm ct
   15.10          val _ = super_theory (theory_of computer) thy
   15.11          val naming = naming_of computer
   15.12          val (encoding, t) = remove_types (encoding_of computer) t'
   15.13 @@ -507,7 +508,7 @@
   15.14      fun compute_inst (s, ct) vs =
   15.15          let
   15.16              val _ = super_theory (Thm.theory_of_cterm ct) thy
   15.17 -            val ty = Thm.typ_of (Thm.ctyp_of_term ct) 
   15.18 +            val ty = Thm.typ_of_cterm ct
   15.19          in          
   15.20              (case Symtab.lookup vartab s of 
   15.21                   NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
    16.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Mar 04 20:50:20 2015 +0100
    16.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Mar 04 22:05:01 2015 +0100
    16.3 @@ -258,7 +258,7 @@
    16.4  
    16.5  local
    16.6   val pth_zero = @{thm norm_zero}
    16.7 - val tv_n = (Thm.ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
    16.8 + val tv_n = (Thm.ctyp_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
    16.9               pth_zero
   16.10   val concl = Thm.dest_arg o Thm.cprop_of
   16.11   fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
   16.12 @@ -319,7 +319,7 @@
   16.13          (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
   16.14  
   16.15    in fst (RealArith.real_linear_prover translator
   16.16 -        (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_term t)],[]) pth_zero)
   16.17 +        (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_cterm t)],[]) pth_zero)
   16.18              zerodests,
   16.19          map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
   16.20                         arg_conv (arg_conv real_poly_conv))) ges',
   16.21 @@ -342,8 +342,8 @@
   16.22    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   16.23    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
   16.24    fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
   16.25 -  fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   16.26 -  fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   16.27 +  fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   16.28 +  fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   16.29    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
   16.30    val replace_conv = try_conv (rewrs_conv asl)
   16.31    val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
    17.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 04 20:50:20 2015 +0100
    17.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 04 22:05:01 2015 +0100
    17.3 @@ -14,7 +14,7 @@
    17.4    let
    17.5      val thy = Thm.theory_of_thm st;
    17.6      val cgoal = nth (cprems_of st) (i - 1);
    17.7 -    val {maxidx, ...} = Thm.rep_cterm cgoal;
    17.8 +    val maxidx = Thm.maxidx_of_cterm cgoal;
    17.9      val j = maxidx + 1;
   17.10      val tyinst' = map (apfst (Logic.incr_tvar j)) tyinst;
   17.11      val ps = Logic.strip_params (Thm.term_of cgoal);
    18.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Mar 04 20:50:20 2015 +0100
    18.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Mar 04 22:05:01 2015 +0100
    18.3 @@ -485,7 +485,7 @@
    18.4                             val (cf, ct) =
    18.5                               Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th));
    18.6                             val arg_cong' = Drule.instantiate'
    18.7 -                             [SOME (Thm.ctyp_of_term ct)]
    18.8 +                             [SOME (Thm.ctyp_of_cterm ct)]
    18.9                               [NONE, SOME ct, SOME cf] (arg_cong RS iffD2);
   18.10                             val inst = Thm.first_order_match (ct,
   18.11                               Thm.dest_arg (Thm.dest_arg (Thm.cprop_of th')))
    19.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Mar 04 20:50:20 2015 +0100
    19.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Mar 04 22:05:01 2015 +0100
    19.3 @@ -433,11 +433,11 @@
    19.4  
    19.5  val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
    19.6  val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
    19.7 -val ct1' = Thm.cterm_of @{theory} (term_of_dB [] (#T (Thm.rep_cterm ct1)) dB1);
    19.8 +val ct1' = Thm.cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
    19.9  
   19.10  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)))))"};
   19.11  val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
   19.12 -val ct2' = Thm.cterm_of @{theory} (term_of_dB [] (#T (Thm.rep_cterm ct2)) dB2);
   19.13 +val ct2' = Thm.cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
   19.14  *}
   19.15  
   19.16  end
    20.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 04 20:50:20 2015 +0100
    20.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 04 22:05:01 2015 +0100
    20.3 @@ -133,8 +133,7 @@
    20.4      fun mtch (env as (tyinsts, insts)) =
    20.5        fn (Var (ixn, T), ct) =>
    20.6            (case AList.lookup (op =) insts ixn of
    20.7 -            NONE =>
    20.8 -              (naive_typ_match (T, Thm.typ_of (Thm.ctyp_of_term ct)) tyinsts, (ixn, ct) :: insts)
    20.9 +            NONE => (naive_typ_match (T, Thm.typ_of_cterm ct) tyinsts, (ixn, ct) :: insts)
   20.10            | SOME _ => env)
   20.11         | (f $ t, ct) =>
   20.12            let val (cf, ct') = Thm.dest_comb ct;
   20.13 @@ -154,7 +153,7 @@
   20.14          (Thm.ctyp_of thy (TVar (v, S)), Thm.ctyp_of thy U)) tyinsts;
   20.15      val insts' =
   20.16        map (fn (idxn, ct) =>
   20.17 -        (Thm.cterm_of thy (Var (idxn, Thm.typ_of (Thm.ctyp_of_term ct))), ct)) insts;
   20.18 +        (Thm.cterm_of thy (Var (idxn, Thm.typ_of_cterm ct)), ct)) insts;
   20.19      val rule' = Thm.instantiate (tyinsts', insts') rule;
   20.20    in fold Thm.elim_implies prems rule' end;
   20.21  
   20.22 @@ -216,19 +215,19 @@
   20.23      fun in_set ps tree =
   20.24        let
   20.25          val (_, [l, x, _, r]) = Drule.strip_comb tree;
   20.26 -        val xT = Thm.ctyp_of_term x;
   20.27 +        val xT = Thm.ctyp_of_cterm x;
   20.28        in
   20.29          (case ps of
   20.30            [] =>
   20.31              instantiate
   20.32 -              [(Thm.ctyp_of_term x_in_set_root, xT)]
   20.33 +              [(Thm.ctyp_of_cterm x_in_set_root, xT)]
   20.34                [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root}
   20.35          | Left :: ps' =>
   20.36              let
   20.37                val in_set_l = in_set ps' l;
   20.38                val in_set_left' =
   20.39                  instantiate
   20.40 -                  [(Thm.ctyp_of_term x_in_set_left, xT)]
   20.41 +                  [(Thm.ctyp_of_cterm x_in_set_left, xT)]
   20.42                    [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left};
   20.43              in discharge [in_set_l] in_set_left' end
   20.44          | Right :: ps' =>
   20.45 @@ -236,7 +235,7 @@
   20.46                val in_set_r = in_set ps' r;
   20.47                val in_set_right' =
   20.48                  instantiate
   20.49 -                  [(Thm.ctyp_of_term x_in_set_right, xT)]
   20.50 +                  [(Thm.ctyp_of_cterm x_in_set_right, xT)]
   20.51                    [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right};
   20.52              in discharge [in_set_r] in_set_right' end)
   20.53        end;
   20.54 @@ -288,7 +287,7 @@
   20.55        val ct =
   20.56          @{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   20.57          |> Thm.dest_comb |> #2;
   20.58 -      val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
   20.59 +      val [alpha] = ct |> Thm.ctyp_of_cterm |> Thm.dest_ctyp;
   20.60      in (alpha, #1 (dest_Var (Thm.term_of ct))) end;
   20.61  in
   20.62  
    21.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Wed Mar 04 20:50:20 2015 +0100
    21.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Wed Mar 04 22:05:01 2015 +0100
    21.3 @@ -713,8 +713,7 @@
    21.4   (i_opt : int option) : thm -> 'a list = fn st =>
    21.5    let
    21.6      val t_raws =
    21.7 -        Thm.rep_thm st
    21.8 -        |> #prop
    21.9 +        Thm.prop_of st
   21.10          |> strip_top_all_vars []
   21.11          |> snd
   21.12          |> Logic.strip_horn
    22.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Mar 04 20:50:20 2015 +0100
    22.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Mar 04 22:05:01 2015 +0100
    22.3 @@ -128,9 +128,9 @@
    22.4          val thy = Proof_Context.theory_of ctxt
    22.5          fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
    22.6          val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
    22.7 -        val typ = (Thm.typ_of o Thm.ctyp_of_term) rel
    22.8 +        val typ = Thm.typ_of_cterm rel
    22.9          val POS_const = Thm.cterm_of thy (mk_POS typ)
   22.10 -        val var = Thm.cterm_of thy (Var (("X", #maxidx (Thm.rep_cterm (rel)) + 1), typ))
   22.11 +        val var = Thm.cterm_of thy (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
   22.12          val goal =
   22.13            Thm.apply (Thm.cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
   22.14        in
   22.15 @@ -513,7 +513,7 @@
   22.16          fun cconl_of thm = Drule.strip_imp_concl (Thm.cprop_of thm)
   22.17          fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
   22.18          fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
   22.19 -        val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
   22.20 +        val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
   22.21          val lhs = lhs_of rule1;
   22.22          val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
   22.23          val rule3 =
    23.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Mar 04 20:50:20 2015 +0100
    23.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Mar 04 22:05:01 2015 +0100
    23.3 @@ -408,7 +408,7 @@
    23.4        val ct =
    23.5          thm |> Thm.cprop_of |> Drule.strip_imp_concl
    23.6          |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
    23.7 -      val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
    23.8 +      val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def
    23.9        val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
   23.10          handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
   23.11      in
    24.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Mar 04 20:50:20 2015 +0100
    24.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Mar 04 22:05:01 2015 +0100
    24.3 @@ -440,7 +440,7 @@
    24.4    
    24.5    fun rewr_imp rule ct = 
    24.6      let
    24.7 -      val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
    24.8 +      val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
    24.9        val lhs_rule = get_lhs rule1;
   24.10        val rule2 = Thm.rename_boundvars (Thm.term_of lhs_rule) (Thm.term_of ct) rule1;
   24.11        val lhs_ct = Thm.dest_fun ct
    25.1 --- a/src/HOL/Tools/Meson/meson.ML	Wed Mar 04 20:50:20 2015 +0100
    25.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Mar 04 22:05:01 2015 +0100
    25.3 @@ -347,7 +347,7 @@
    25.4    assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
    25.5  local  
    25.6    val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
    25.7 -  val spec_varT = #T (Thm.rep_cterm spec_var);
    25.8 +  val spec_varT = Thm.typ_of_cterm spec_var;
    25.9    fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
   25.10  in  
   25.11    fun freeze_spec th ctxt =
    26.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Mar 04 20:50:20 2015 +0100
    26.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Mar 04 22:05:01 2015 +0100
    26.3 @@ -103,7 +103,7 @@
    26.4    let
    26.5        val thy = Thm.theory_of_cterm ct
    26.6        val Abs(x,_,body) = Thm.term_of ct
    26.7 -      val Type(@{type_name fun}, [xT,bodyT]) = Thm.typ_of (Thm.ctyp_of_term ct)
    26.8 +      val Type (@{type_name fun}, [xT,bodyT]) = Thm.typ_of_cterm ct
    26.9        val cxT = Thm.ctyp_of thy xT
   26.10        val cbodyT = Thm.ctyp_of thy bodyT
   26.11        fun makeK () =
    27.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Wed Mar 04 20:50:20 2015 +0100
    27.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Wed Mar 04 22:05:01 2015 +0100
    27.3 @@ -49,7 +49,7 @@
    27.4        Const (@{const_name HOL.eq}, _) $ _ $ t =>
    27.5        let
    27.6          val ct = Thm.cterm_of thy t
    27.7 -        val cT = Thm.ctyp_of_term ct
    27.8 +        val cT = Thm.ctyp_of_cterm ct
    27.9        in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
   27.10      | Const (@{const_name disj}, _) $ t1 $ t2 =>
   27.11        (if can HOLogic.dest_not t1 then t2 else t1)
    28.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Mar 04 20:50:20 2015 +0100
    28.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Mar 04 22:05:01 2015 +0100
    28.3 @@ -760,7 +760,7 @@
    28.4   | _ => is_number t orelse can HOLogic.dest_nat t
    28.5  
    28.6   fun ty cts t = 
    28.7 -  if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of (Thm.ctyp_of_term t)))
    28.8 +  if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t))
    28.9    then false 
   28.10    else case Thm.term_of t of 
   28.11      c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
   28.12 @@ -800,7 +800,7 @@
   28.13  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
   28.14   let 
   28.15     fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
   28.16 -   fun gen x t = Thm.apply (all (Thm.ctyp_of_term x)) (Thm.lambda x t)
   28.17 +   fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
   28.18     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
   28.19     val p' = fold_rev gen ts p
   28.20   in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
    29.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Mar 04 20:50:20 2015 +0100
    29.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Mar 04 22:05:01 2015 +0100
    29.3 @@ -73,7 +73,7 @@
    29.4  val lhs = eq |> Thm.dest_arg1;
    29.5  val pt_random_aux = lhs |> Thm.dest_fun;
    29.6  val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
    29.7 -val aT = pt_random_aux |> Thm.ctyp_of_term |> dest_ctyp_nth 1;
    29.8 +val aT = pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1;
    29.9  
   29.10  val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one},
   29.11    @{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}];
    30.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Mar 04 20:50:20 2015 +0100
    30.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Mar 04 22:05:01 2015 +0100
    30.3 @@ -541,7 +541,7 @@
    30.4  (* Tactic for Generalising Free Variables in a Goal *)
    30.5  
    30.6  fun inst_spec ctrm =
    30.7 -  Drule.instantiate' [SOME (Thm.ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
    30.8 +  Drule.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
    30.9  
   30.10  fun inst_spec_tac ctrms =
   30.11    EVERY' (map (dtac o inst_spec) ctrms)
    31.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed Mar 04 20:50:20 2015 +0100
    31.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Mar 04 22:05:01 2015 +0100
    31.3 @@ -89,7 +89,7 @@
    31.4    mk_builtin_typ = z3_mk_builtin_typ,
    31.5    mk_builtin_num = z3_mk_builtin_num,
    31.6    mk_builtin_fun = (fn _ => fn sym => fn cts =>
    31.7 -    (case try (#T o Thm.rep_cterm o hd) cts of
    31.8 +    (case try (Thm.typ_of_cterm o hd) cts of
    31.9        SOME @{typ real} => z3_mk_builtin_fun sym cts
   31.10      | _ => NONE)) }
   31.11  
    32.1 --- a/src/HOL/Tools/SMT/smt_util.ML	Wed Mar 04 20:50:20 2015 +0100
    32.2 +++ b/src/HOL/Tools/SMT/smt_util.ML	Wed Mar 04 22:05:01 2015 +0100
    32.3 @@ -45,7 +45,6 @@
    32.4    val instT': cterm -> ctyp * cterm -> cterm
    32.5  
    32.6    (*certified terms*)
    32.7 -  val typ_of: cterm -> typ
    32.8    val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
    32.9    val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
   32.10    val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
   32.11 @@ -167,20 +166,18 @@
   32.12  
   32.13  fun mk_const_pat thy name destT =
   32.14    let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
   32.15 -  in (destT (Thm.ctyp_of_term cpat), cpat) end
   32.16 +  in (destT (Thm.ctyp_of_cterm cpat), cpat) end
   32.17  
   32.18  val destT1 = hd o Thm.dest_ctyp
   32.19  val destT2 = hd o tl o Thm.dest_ctyp
   32.20  
   32.21  fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
   32.22  fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
   32.23 -fun instT' ct = instT (Thm.ctyp_of_term ct)
   32.24 +fun instT' ct = instT (Thm.ctyp_of_cterm ct)
   32.25  
   32.26  
   32.27  (* certified terms *)
   32.28  
   32.29 -fun typ_of ct = #T (Thm.rep_cterm ct)
   32.30 -
   32.31  fun dest_cabs ct ctxt =
   32.32    (case Thm.term_of ct of
   32.33      Abs _ =>
    33.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Mar 04 20:50:20 2015 +0100
    33.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Mar 04 22:05:01 2015 +0100
    33.3 @@ -136,7 +136,7 @@
    33.4  val update =
    33.5    SMT_Util.mk_const_pat @{theory} @{const_name fun_upd} (Thm.dest_ctyp o SMT_Util.destT1)
    33.6  fun mk_update array index value =
    33.7 -  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
    33.8 +  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
    33.9    in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
   33.10  
   33.11  val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
   33.12 @@ -166,7 +166,7 @@
   33.13    | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
   33.14    | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
   33.15    | _ =>
   33.16 -    (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
   33.17 +    (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of
   33.18        (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
   33.19      | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
   33.20      | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
    34.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Wed Mar 04 20:50:20 2015 +0100
    34.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Wed Mar 04 22:05:01 2015 +0100
    34.3 @@ -70,7 +70,7 @@
    34.4  val mk_hol_const = Thm.cterm_of @{theory HOL} o Const;
    34.5  
    34.6  fun mk_exists (r as (Bvar, Body)) =
    34.7 -  let val ty = #T(Thm.rep_cterm Bvar)
    34.8 +  let val ty = Thm.typ_of_cterm Bvar
    34.9        val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
   34.10    in capply c (uncurry cabs r) end;
   34.11  
   34.12 @@ -88,12 +88,12 @@
   34.13   * The primitives.
   34.14   *---------------------------------------------------------------------------*)
   34.15  fun dest_const ctm =
   34.16 -   (case #t(Thm.rep_cterm ctm)
   34.17 +   (case Thm.term_of ctm
   34.18        of Const(s,ty) => {Name = s, Ty = ty}
   34.19         | _ => raise ERR "dest_const" "not a constant");
   34.20  
   34.21  fun dest_var ctm =
   34.22 -   (case #t(Thm.rep_cterm ctm)
   34.23 +   (case Thm.term_of ctm
   34.24        of Var((s,i),ty) => {Name=s, Ty=ty}
   34.25         | Free(s,ty)    => {Name=s, Ty=ty}
   34.26         |             _ => raise ERR "dest_var" "not a variable");
    35.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Mar 04 20:50:20 2015 +0100
    35.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Mar 04 22:05:01 2015 +0100
    35.3 @@ -121,7 +121,7 @@
    35.4  
    35.5  
    35.6  fun FILTER_DISCH_ALL P thm =
    35.7 - let fun check tm = P (#t (Thm.rep_cterm tm))
    35.8 + let fun check tm = P (Thm.term_of tm)
    35.9   in  fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
   35.10   end;
   35.11  
   35.12 @@ -269,7 +269,7 @@
   35.13        val gspec = Thm.forall_intr (Thm.cterm_of thy x) spec
   35.14  in
   35.15  fun SPEC tm thm =
   35.16 -   let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_term tm)], []) gspec
   35.17 +   let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec
   35.18     in thm RS (Thm.forall_elim tm gspec') end
   35.19  end;
   35.20  
   35.21 @@ -285,7 +285,7 @@
   35.22        fun cty_theta s = map (fn (i, (S, ty)) => (Thm.ctyp_of s (TVar (i, S)), Thm.ctyp_of s ty))
   35.23        fun ctm_theta s = map (fn (i, (_, tm2)) =>
   35.24                               let val ctm2 = Thm.cterm_of s tm2
   35.25 -                             in (Thm.cterm_of s (Var(i,#T(Thm.rep_cterm ctm2))), ctm2)
   35.26 +                             in (Thm.cterm_of s (Var(i, Thm.typ_of_cterm ctm2)), ctm2)
   35.27                               end)
   35.28        fun certify s (ty_theta,tm_theta) =
   35.29          (cty_theta s (Vartab.dest ty_theta),
    36.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Wed Mar 04 20:50:20 2015 +0100
    36.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Wed Mar 04 22:05:01 2015 +0100
    36.3 @@ -195,7 +195,7 @@
    36.4      | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
    36.5  
    36.6  fun Rel_conv ct =
    36.7 -  let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
    36.8 +  let val (cT, cT') = dest_funcT (Thm.ctyp_of_cterm ct)
    36.9        val (cU, _) = dest_funcT cT'
   36.10    in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
   36.11  
   36.12 @@ -441,8 +441,8 @@
   36.13            val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
   36.14            val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
   36.15            val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
   36.16 -          val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_term r1))
   36.17 -          val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_term r2))
   36.18 +          val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
   36.19 +          val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
   36.20            val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
   36.21            val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
   36.22            val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
    37.1 --- a/src/HOL/Tools/choice_specification.ML	Wed Mar 04 20:50:20 2015 +0100
    37.2 +++ b/src/HOL/Tools/choice_specification.ML	Wed Mar 04 22:05:01 2015 +0100
    37.3 @@ -137,7 +137,7 @@
    37.4          fun inst_all thy v thm =
    37.5            let
    37.6              val cv = Thm.cterm_of thy v
    37.7 -            val cT = Thm.ctyp_of_term cv
    37.8 +            val cT = Thm.ctyp_of_cterm cv
    37.9              val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
   37.10            in thm RS spec' end
   37.11          fun remove_alls frees thm = fold (inst_all (Thm.theory_of_thm thm)) frees thm
    38.1 --- a/src/HOL/Tools/groebner.ML	Wed Mar 04 20:50:20 2015 +0100
    38.2 +++ b/src/HOL/Tools/groebner.ML	Wed Mar 04 22:05:01 2015 +0100
    38.3 @@ -435,7 +435,7 @@
    38.4  
    38.5  fun sym_conv eq =
    38.6   let val (l,r) = Thm.dest_binop eq
    38.7 - in instantiate' [SOME (Thm.ctyp_of_term l)] [SOME l, SOME r] eq_commute
    38.8 + in instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute
    38.9   end;
   38.10  
   38.11    (* FIXME : copied from cqe.ML -- complex QE*)
   38.12 @@ -479,13 +479,13 @@
   38.13     (* Conversion for the equivalence of existential statements where
   38.14        EX quantifiers are rearranged differently *)
   38.15   fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   38.16 - fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_term v)) (Thm.lambda v t)
   38.17 + fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
   38.18  
   38.19  fun choose v th th' = case Thm.concl_of th of
   38.20    @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
   38.21     let
   38.22      val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
   38.23 -    val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_term) p
   38.24 +    val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
   38.25      val th0 = Conv.fconv_rule (Thm.beta_conversion true)
   38.26          (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   38.27      val pv = (Thm.rhs_of o Thm.beta_conversion true)
   38.28 @@ -504,7 +504,7 @@
   38.29     val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
   38.30    in Thm.implies_elim
   38.31      (Conv.fconv_rule (Thm.beta_conversion true)
   38.32 -      (instantiate' [SOME (Thm.ctyp_of_term v)] [SOME p, SOME v] @{thm exI}))
   38.33 +      (instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
   38.34        th
   38.35    end
   38.36   fun ex_eq_conv t =
   38.37 @@ -527,7 +527,7 @@
   38.38   | Var ((s,_),_) => s
   38.39   | _ => "x"
   38.40   fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
   38.41 -  fun mk_exists v th = Drule.arg_cong_rule (ext (Thm.ctyp_of_term v))
   38.42 +  fun mk_exists v th = Drule.arg_cong_rule (ext (Thm.ctyp_of_cterm v))
   38.43     (Thm.abstract_rule (getname v) v th)
   38.44   fun simp_ex_conv ctxt =
   38.45     Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
   38.46 @@ -739,7 +739,7 @@
   38.47   let
   38.48    fun mk_forall x p =
   38.49      Thm.apply
   38.50 -      (Drule.cterm_rule (instantiate' [SOME (Thm.ctyp_of_term x)] [])
   38.51 +      (Drule.cterm_rule (instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
   38.52          @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
   38.53    val avs = Thm.add_cterm_frees tm []
   38.54    val P' = fold mk_forall avs tm
   38.55 @@ -919,7 +919,7 @@
   38.56    | SOME (res as (theory, {is_const = _, dest_const,
   38.57            mk_const, conv = ring_eq_conv})) =>
   38.58       SOME (ring_and_ideal_conv theory
   38.59 -          dest_const (mk_const (Thm.ctyp_of_term tm)) (ring_eq_conv ctxt)
   38.60 +          dest_const (mk_const (Thm.ctyp_of_cterm tm)) (ring_eq_conv ctxt)
   38.61            (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)))
   38.62  
   38.63  fun presimplify ctxt add_thms del_thms =
   38.64 @@ -945,7 +945,7 @@
   38.65    Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
   38.66   | _=> raise CTERM ("ideal_tac - lhs",[t])
   38.67   fun exitac NONE = no_tac
   38.68 -   | exitac (SOME y) = rtac (instantiate' [SOME (Thm.ctyp_of_term y)] [NONE,SOME y] exI) 1
   38.69 +   | exitac (SOME y) = rtac (instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI) 1
   38.70  
   38.71   val claset = claset_of @{context}
   38.72  in
    39.1 --- a/src/HOL/Tools/int_arith.ML	Wed Mar 04 20:50:20 2015 +0100
    39.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Mar 04 22:05:01 2015 +0100
    39.3 @@ -25,7 +25,7 @@
    39.4  val lhss0 = [@{cpat "0::?'a::ring"}];
    39.5  
    39.6  fun proc0 phi ctxt ct =
    39.7 -  let val T = Thm.ctyp_of_term ct
    39.8 +  let val T = Thm.ctyp_of_cterm ct
    39.9    in if Thm.typ_of T = @{typ int} then NONE else
   39.10       SOME (instantiate' [SOME T] [] zeroth)
   39.11    end;
   39.12 @@ -39,7 +39,7 @@
   39.13  val lhss1 = [@{cpat "1::?'a::ring_1"}];
   39.14  
   39.15  fun proc1 phi ctxt ct =
   39.16 -  let val T = Thm.ctyp_of_term ct
   39.17 +  let val T = Thm.ctyp_of_cterm ct
   39.18    in if Thm.typ_of T = @{typ int} then NONE else
   39.19       SOME (instantiate' [SOME T] [] oneth)
   39.20    end;
    40.1 --- a/src/HOL/Tools/legacy_transfer.ML	Wed Mar 04 20:50:20 2015 +0100
    40.2 +++ b/src/HOL/Tools/legacy_transfer.ML	Wed Mar 04 22:05:01 2015 +0100
    40.3 @@ -89,7 +89,7 @@
    40.4      val tys = map snd (Term.add_vars t []);
    40.5      val _ = if null tys then error "Transfer: unable to guess instance" else ();
    40.6      val tyss = splits (curry Type.could_unify) tys;
    40.7 -    val get_ty = Thm.typ_of o Thm.ctyp_of_term o fst o direction_of;
    40.8 +    val get_ty = Thm.typ_of_cterm o fst o direction_of;
    40.9      val insts = map_filter (fn tys => get_first (fn (k, e) =>
   40.10        if Type.could_unify (hd tys, range_type (get_ty k))
   40.11        then SOME (direction_of k, transfer_rules_of e)
   40.12 @@ -108,7 +108,7 @@
   40.13        |> Variable.import true (map Drule.mk_term [raw_a, raw_D])
   40.14        |>> map Drule.dest_term o snd;
   40.15      val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
   40.16 -    val T = Thm.typ_of (Thm.ctyp_of_term a);
   40.17 +    val T = Thm.typ_of_cterm a;
   40.18      val (aT, bT) = (Term.range_type T, Term.domain_type T);
   40.19  
   40.20      (* determine variables to transfer *)
    41.1 --- a/src/HOL/Tools/numeral.ML	Wed Mar 04 20:50:20 2015 +0100
    41.2 +++ b/src/HOL/Tools/numeral.ML	Wed Mar 04 22:05:01 2015 +0100
    41.3 @@ -38,16 +38,16 @@
    41.4  local
    41.5  
    41.6  val zero = @{cpat "0"};
    41.7 -val zeroT = Thm.ctyp_of_term zero;
    41.8 +val zeroT = Thm.ctyp_of_cterm zero;
    41.9  
   41.10  val one = @{cpat "1"};
   41.11 -val oneT = Thm.ctyp_of_term one;
   41.12 +val oneT = Thm.ctyp_of_cterm one;
   41.13  
   41.14  val numeral = @{cpat "numeral"};
   41.15 -val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
   41.16 +val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
   41.17  
   41.18  val uminus = @{cpat "uminus"};
   41.19 -val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus)));
   41.20 +val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
   41.21  
   41.22  fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
   41.23  
    42.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Mar 04 20:50:20 2015 +0100
    42.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Mar 04 22:05:01 2015 +0100
    42.3 @@ -587,9 +587,9 @@
    42.4  
    42.5  local
    42.6   val zr = @{cpat "0"}
    42.7 - val zT = Thm.ctyp_of_term zr
    42.8 + val zT = Thm.ctyp_of_cterm zr
    42.9   val geq = @{cpat HOL.eq}
   42.10 - val eqT = Thm.dest_ctyp (Thm.ctyp_of_term geq) |> hd
   42.11 + val eqT = Thm.dest_ctyp (Thm.ctyp_of_cterm geq) |> hd
   42.12   val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
   42.13   val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
   42.14   val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
   42.15 @@ -609,7 +609,7 @@
   42.16      val ((x,y),(w,z)) =
   42.17           (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
   42.18      val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w]
   42.19 -    val T = Thm.ctyp_of_term x
   42.20 +    val T = Thm.ctyp_of_cterm x
   42.21      val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
   42.22      val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
   42.23    in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
   42.24 @@ -619,7 +619,7 @@
   42.25   fun proc2 phi ctxt ct =
   42.26    let
   42.27      val (l,r) = Thm.dest_binop ct
   42.28 -    val T = Thm.ctyp_of_term l
   42.29 +    val T = Thm.ctyp_of_cterm l
   42.30    in (case (Thm.term_of l, Thm.term_of r) of
   42.31        (Const(@{const_name Fields.divide},_)$_$_, _) =>
   42.32          let val (x,y) = Thm.dest_binop l val z = r
   42.33 @@ -648,42 +648,42 @@
   42.34        let
   42.35          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   42.36          val _ = map is_number [a,b,c]
   42.37 -        val T = Thm.ctyp_of_term c
   42.38 +        val T = Thm.ctyp_of_cterm c
   42.39          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
   42.40        in SOME (mk_meta_eq th) end
   42.41    | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
   42.42        let
   42.43          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   42.44          val _ = map is_number [a,b,c]
   42.45 -        val T = Thm.ctyp_of_term c
   42.46 +        val T = Thm.ctyp_of_cterm c
   42.47          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   42.48        in SOME (mk_meta_eq th) end
   42.49    | Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
   42.50        let
   42.51          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   42.52          val _ = map is_number [a,b,c]
   42.53 -        val T = Thm.ctyp_of_term c
   42.54 +        val T = Thm.ctyp_of_cterm c
   42.55          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   42.56        in SOME (mk_meta_eq th) end
   42.57    | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
   42.58      let
   42.59        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   42.60          val _ = map is_number [a,b,c]
   42.61 -        val T = Thm.ctyp_of_term c
   42.62 +        val T = Thm.ctyp_of_cterm c
   42.63          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   42.64        in SOME (mk_meta_eq th) end
   42.65    | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
   42.66      let
   42.67        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   42.68          val _ = map is_number [a,b,c]
   42.69 -        val T = Thm.ctyp_of_term c
   42.70 +        val T = Thm.ctyp_of_cterm c
   42.71          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   42.72        in SOME (mk_meta_eq th) end
   42.73    | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
   42.74      let
   42.75        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   42.76          val _ = map is_number [a,b,c]
   42.77 -        val T = Thm.ctyp_of_term c
   42.78 +        val T = Thm.ctyp_of_cterm c
   42.79          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   42.80        in SOME (mk_meta_eq th) end
   42.81    | _ => NONE)
    43.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 04 20:50:20 2015 +0100
    43.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 04 22:05:01 2015 +0100
    43.3 @@ -522,7 +522,7 @@
    43.4            let
    43.5              val cv = mth |> Thm.cprop_of |> Drule.strip_imp_concl
    43.6                |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg1
    43.7 -            val T = #T (Thm.rep_cterm cv)
    43.8 +            val T = Thm.typ_of_cterm cv
    43.9            in
   43.10              mth
   43.11              |> Thm.instantiate ([], [(cv, number_of T n)])
    44.1 --- a/src/Pure/conv.ML	Wed Mar 04 20:50:20 2015 +0100
    44.2 +++ b/src/Pure/conv.ML	Wed Mar 04 22:05:01 2015 +0100
    44.3 @@ -158,7 +158,7 @@
    44.4  
    44.5  fun rewr_conv rule ct =
    44.6    let
    44.7 -    val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
    44.8 +    val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
    44.9      val lhs = Thm.lhs_of rule1;
   44.10      val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
   44.11      val rule3 =
    45.1 --- a/src/Pure/drule.ML	Wed Mar 04 20:50:20 2015 +0100
    45.2 +++ b/src/Pure/drule.ML	Wed Mar 04 22:05:01 2015 +0100
    45.3 @@ -649,7 +649,7 @@
    45.4      val thy = Thm.theory_of_cterm ct;
    45.5      val cert = Thm.cterm_of thy;
    45.6      val certT = Thm.ctyp_of thy;
    45.7 -    val T = Thm.typ_of (Thm.ctyp_of_term ct);
    45.8 +    val T = Thm.typ_of_cterm ct;
    45.9      val a = certT (TVar (("'a", 0), []));
   45.10      val x = cert (Var (("x", 0), T));
   45.11    in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
    46.1 --- a/src/Pure/more_thm.ML	Wed Mar 04 20:50:20 2015 +0100
    46.2 +++ b/src/Pure/more_thm.ML	Wed Mar 04 22:05:01 2015 +0100
    46.3 @@ -126,7 +126,7 @@
    46.4  fun all_name (x, t) A =
    46.5    let
    46.6      val cert = Thm.cterm_of (Thm.theory_of_cterm t);
    46.7 -    val T = #T (Thm.rep_cterm t);
    46.8 +    val T = Thm.typ_of_cterm t;
    46.9    in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
   46.10  
   46.11  fun all t A = all_name ("", t) A;
    47.1 --- a/src/Pure/raw_simplifier.ML	Wed Mar 04 20:50:20 2015 +0100
    47.2 +++ b/src/Pure/raw_simplifier.ML	Wed Mar 04 22:05:01 2015 +0100
    47.3 @@ -1293,7 +1293,7 @@
    47.4      val thy = Proof_Context.theory_of raw_ctxt;
    47.5  
    47.6      val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
    47.7 -    val {maxidx, ...} = Thm.rep_cterm ct;
    47.8 +    val maxidx = Thm.maxidx_of_cterm ct;
    47.9      val _ =
   47.10        Theory.subthy (Thm.theory_of_cterm ct, thy) orelse
   47.11          raise CTERM ("rewrite_cterm: bad background theory", [ct]);
    48.1 --- a/src/Pure/subgoal.ML	Wed Mar 04 20:50:20 2015 +0100
    48.2 +++ b/src/Pure/subgoal.ML	Wed Mar 04 22:05:01 2015 +0100
    48.3 @@ -70,7 +70,7 @@
    48.4      val cert = Proof_Context.cterm_of ctxt;
    48.5      val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    48.6  
    48.7 -    val Ts = map (#T o Thm.rep_cterm) params;
    48.8 +    val Ts = map Thm.typ_of_cterm params;
    48.9      val ts = map Thm.term_of params;
   48.10  
   48.11      val prop = Thm.full_prop_of th';
    49.1 --- a/src/Pure/thm.ML	Wed Mar 04 20:50:20 2015 +0100
    49.2 +++ b/src/Pure/thm.ML	Wed Mar 04 22:05:01 2015 +0100
    49.3 @@ -33,7 +33,9 @@
    49.4    val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
    49.5    val theory_of_cterm: cterm -> theory
    49.6    val term_of: cterm -> term
    49.7 -  val ctyp_of_term: cterm -> ctyp
    49.8 +  val typ_of_cterm: cterm -> typ
    49.9 +  val ctyp_of_cterm: cterm -> ctyp
   49.10 +  val maxidx_of_cterm: cterm -> int
   49.11    val cterm_of: theory -> term -> cterm
   49.12    val dest_comb: cterm -> cterm * cterm
   49.13    val dest_fun: cterm -> cterm
   49.14 @@ -186,9 +188,13 @@
   49.15  fun theory_of_cterm (Cterm {thy, ...}) = thy;
   49.16  fun term_of (Cterm {t, ...}) = t;
   49.17  
   49.18 -fun ctyp_of_term (Cterm {thy, T, maxidx, sorts, ...}) =
   49.19 +fun typ_of_cterm (Cterm {T, ...}) = T;
   49.20 +
   49.21 +fun ctyp_of_cterm (Cterm {thy, T, maxidx, sorts, ...}) =
   49.22    Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts};
   49.23  
   49.24 +fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx;
   49.25 +
   49.26  fun cterm_of thy tm =
   49.27    let
   49.28      val (t, T, maxidx) = Sign.certify_term thy tm;
    50.1 --- a/src/Tools/atomize_elim.ML	Wed Mar 04 20:50:20 2015 +0100
    50.2 +++ b/src/Tools/atomize_elim.ML	Wed Mar 04 22:05:01 2015 +0100
    50.3 @@ -117,7 +117,7 @@
    50.4            if is_Bound thesis then all_tac
    50.5            else let
    50.6                val cthesis = Thm.cterm_of thy thesis
    50.7 -              val rule = instantiate' [SOME (Thm.ctyp_of_term cthesis)] [NONE, SOME cthesis]
    50.8 +              val rule = instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
    50.9                           @{thm meta_spec}
   50.10              in
   50.11                compose_tac ctxt (false, rule, 1) i
    51.1 --- a/src/Tools/induct.ML	Wed Mar 04 20:50:20 2015 +0100
    51.2 +++ b/src/Tools/induct.ML	Wed Mar 04 22:05:01 2015 +0100
    51.3 @@ -398,9 +398,9 @@
    51.4      fun prep_var (x, SOME t) =
    51.5            let
    51.6              val cx = cert x;
    51.7 -            val xT = #T (Thm.rep_cterm cx);
    51.8 +            val xT = Thm.typ_of_cterm cx;
    51.9              val ct = cert (tune t);
   51.10 -            val tT = #T (Thm.rep_cterm ct);
   51.11 +            val tT = Thm.typ_of_cterm ct;
   51.12            in
   51.13              if Type.could_unify (tT, xT) then SOME (cx, ct)
   51.14              else error (Pretty.string_of (Pretty.block
   51.15 @@ -576,7 +576,7 @@
   51.16      val pairs = Vartab.dest (Envir.term_env env);
   51.17      val types = Vartab.dest (Envir.type_env env);
   51.18      val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
   51.19 -    val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
   51.20 +    val xs = map2 (curry (cert o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
   51.21    in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
   51.22  
   51.23  in
    52.1 --- a/src/Tools/nbe.ML	Wed Mar 04 20:50:20 2015 +0100
    52.2 +++ b/src/Tools/nbe.ML	Wed Mar 04 22:05:01 2015 +0100
    52.3 @@ -581,7 +581,7 @@
    52.4  fun mk_equals ctxt lhs raw_rhs =
    52.5    let
    52.6      val thy = Proof_Context.theory_of ctxt;
    52.7 -    val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
    52.8 +    val ty = Thm.typ_of_cterm lhs;
    52.9      val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
   52.10      val rhs = Thm.cterm_of thy raw_rhs;
   52.11    in Thm.mk_binop eq lhs rhs end;