src/Pure/meta_simplifier.ML
changeset 10767 8fa4aafa7314
parent 10413 0e015d9bea4e
child 11291 02db0084a695
--- a/src/Pure/meta_simplifier.ML	Wed Jan 03 11:14:48 2001 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Jan 03 21:18:31 2001 +0100
@@ -696,7 +696,7 @@
        (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
@@ -719,7 +719,7 @@
                        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 =>
@@ -742,7 +742,7 @@
                           (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)