# HG changeset patch
# User wenzelm
# Date 1425503101 -3600
# Node ID ddf6deaadfe872efba92dc3032eadd1b5cb26db4
# Parent  68a770a8a09fd2d61c903731b4f72e9517b98117
clarified signature;

diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Decision_Procs/langford.ML
--- 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));
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/HOL.thy
--- 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;
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/HOLCF/Cfun.thy
--- 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};
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Import/import_rule.ML
--- 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]
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Library/Code_Abstract_Nat.thy
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Library/Old_SMT/old_smt_real.ML
--- 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)) }
 
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Library/Old_SMT/old_smt_utils.ML
--- 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 _ =>
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Library/Old_SMT/old_z3_interface.ML
--- 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)
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Library/Old_SMT/old_z3_proof_parser.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
--- 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')
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Library/positivstellensatz.ML
--- 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)
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Matrix_LP/Compute_Oracle/compute.ML
--- 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")
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Multivariate_Analysis/normarith.ML
--- 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))
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Nominal/nominal_fresh_fun.ML
--- 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);
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Nominal/nominal_inductive.ML
--- 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')))
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Proofs/Lambda/WeakNorm.thy
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Statespace/distinct_tree_prover.ML
--- 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
 
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Lifting/lifting_def.ML
--- 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 =
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Lifting/lifting_setup.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Lifting/lifting_term.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Meson/meson.ML
--- 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 =
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Meson/meson_clausify.ML
--- 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 () =
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Metis/metis_tactic.ML
--- 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)
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Qelim/cooper.ML
--- 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));
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Quickcheck/random_generators.ML
--- 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}];
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Quotient/quotient_tacs.ML
--- 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)
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/SMT/smt_real.ML
--- 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)) }
 
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/SMT/smt_util.ML
--- 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 _ =>
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/SMT/z3_interface.ML
--- 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)
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/TFL/dcterm.ML
--- 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");
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/TFL/rules.ML
--- 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),
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Transfer/transfer.ML
--- 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}
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/choice_specification.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/groebner.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/int_arith.ML
--- 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;
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/legacy_transfer.ML
--- 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 *)
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/numeral.ML
--- 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)], []);
 
diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/numeral_simprocs.ML
--- 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)
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Provers/Arith/fast_lin_arith.ML
--- 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)])
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Pure/conv.ML
--- 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 =
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Pure/drule.ML
--- 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;
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Pure/more_thm.ML
--- 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;
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Pure/raw_simplifier.ML
--- 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]);
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Pure/subgoal.ML
--- 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';
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Pure/thm.ML
--- 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;
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Tools/atomize_elim.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Tools/induct.ML
--- 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
diff -r 68a770a8a09f -r ddf6deaadfe8 src/Tools/nbe.ML
--- 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;