# HG changeset patch
# User wenzelm
# Date 898781561 -7200
# Node ID 7274f7d101ee5f04a2df3694fb655eaef4352340
# Parent  ce093ff0880e356d9bfc9203efba76283ff08293
Thm.rewrite_cterm;

diff -r ce093ff0880e -r 7274f7d101ee TFL/rules.new.sml
--- a/TFL/rules.new.sml	Thu Jun 25 15:22:05 1998 +0200
+++ b/TFL/rules.new.sml	Thu Jun 25 15:32:41 1998 +0200
@@ -390,7 +390,7 @@
 fun SUBS thl = 
    rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
 
-local fun rew_conv mss = rewrite_cterm (true,false,false) mss (K(K None))
+local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None))
 in
 fun simpl_conv ss thl ctm = 
  rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
@@ -654,7 +654,7 @@
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
                      val mss' = add_prems(mss, map ASSUME ants)
-                     val lhs_eq_lhs1 = rewrite_cterm(false,true,false)mss' prover lhs
+                     val lhs_eq_lhs1 = Thm.rewrite_cterm(false,true,false)mss' prover lhs
                        handle _ => reflexive lhs
                      val dummy = print_thms "proven:\n" [lhs_eq_lhs1]
                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
@@ -676,7 +676,7 @@
                   val QeqQ1 = pbeta_reduce (tych Q)
                   val Q1 = #2(D.dest_eq(cconcl QeqQ1))
                   val mss' = add_prems(mss, map ASSUME ants1)
-                  val Q1eeqQ2 = rewrite_cterm (false,true,false) mss' prover Q1
+                  val Q1eeqQ2 = Thm.rewrite_cterm (false,true,false) mss' prover Q1
                                 handle _ => reflexive Q1
                   val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
@@ -701,7 +701,7 @@
                  let val tych = cterm_of sign
                      val ants1 = map tych ants
                      val mss' = add_prems(mss, map ASSUME ants1)
-                     val Q_eeq_Q1 = rewrite_cterm(false,true,false) mss' 
+                     val Q_eeq_Q1 = Thm.rewrite_cterm(false,true,false) mss' 
                                                      prover (tych Q)
                       handle _ => reflexive (tych Q)
                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
@@ -771,7 +771,7 @@
     (if (is_cong thm) then cong_prover else restrict_prover) mss thm
     end
     val ctm = cprop_of th
-    val th1 = rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs))
+    val th1 = Thm.rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs))
                             prover ctm
     val th2 = equal_elim th1 th
  in