src/Pure/meta_simplifier.ML

     and subc skel
           (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) t0 =
        (case term_of t0 of
            Abs (a, T, t) =>
              let val b = variant bounds a
-                 val (v, t') = dest_abs (Some ("." ^ b)) t0
+                 val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
              in case botc skel' mss' t' of
                   Some thm => Some (abstract_rule a v thm)
                 | None => None

                let fun appc () =
                      let
                        val (tskel, uskel) = case skel of
                            tskel $ uskel => (tskel, uskel)
                          | _ => (skel0, skel0);
-                       val (ct, cu) = dest_comb t0
+                       val (ct, cu) = Thm.dest_comb t0
                      in
                      (case botc tskel mss ct of
                         Some thm1 =>
                           (case botc uskel mss cu of
                              Some thm2 => Some (combination thm1 thm2)

 (* post processing: some partial applications h t1 ... tj, j <= length ts,
    may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
                           (let
                              val thm = congc (prover mss, sign, maxidx) cong t0;
                              val t = rhs_of thm;
-                             val (cl, cr) = dest_comb t
+                             val (cl, cr) = Thm.dest_comb t
                              val dVar = Var(("", 0), dummyT)
                              val skel =
                                list_comb (h, replicate (length ts) dVar)
                            in case botc skel mss cl of
                                 None => Some thm