src/Pure/meta_simplifier.ML
changeset 10767 8fa4aafa7314
parent 10413 0e015d9bea4e
child 11291 02db0084a695
     1.1 --- a/src/Pure/meta_simplifier.ML	Wed Jan 03 11:14:48 2001 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Wed Jan 03 21:18:31 2001 +0100
     1.3 @@ -696,7 +696,7 @@
     1.4         (case term_of t0 of
     1.5             Abs (a, T, t) =>
     1.6               let val b = variant bounds a
     1.7 -                 val (v, t') = dest_abs (Some ("." ^ b)) t0
     1.8 +                 val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
     1.9                   val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
    1.10                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
    1.11               in case botc skel' mss' t' of
    1.12 @@ -719,7 +719,7 @@
    1.13                         val (tskel, uskel) = case skel of
    1.14                             tskel $ uskel => (tskel, uskel)
    1.15                           | _ => (skel0, skel0);
    1.16 -                       val (ct, cu) = dest_comb t0
    1.17 +                       val (ct, cu) = Thm.dest_comb t0
    1.18                       in
    1.19                       (case botc tskel mss ct of
    1.20                          Some thm1 =>
    1.21 @@ -742,7 +742,7 @@
    1.22                            (let
    1.23                               val thm = congc (prover mss, sign, maxidx) cong t0;
    1.24                               val t = rhs_of thm;
    1.25 -                             val (cl, cr) = dest_comb t
    1.26 +                             val (cl, cr) = Thm.dest_comb t
    1.27                               val dVar = Var(("", 0), dummyT)
    1.28                               val skel =
    1.29                                 list_comb (h, replicate (length ts) dVar)