# HG changeset patch
# User berghofe
# Date 973615992 -3600
# Node ID 42e6b8502d52e1611bff96f1cd3571f90b5ce790
# Parent  5b33e732e459ed03ed2355ba3e09a92551e8bcdf
Moved rewriting functions from Thm to MetaSimplifier.

diff -r 5b33e732e459 -r 42e6b8502d52 TFL/rules.sml
--- a/TFL/rules.sml	Tue Nov 07 17:52:12 2000 +0100
+++ b/TFL/rules.sml	Tue Nov 07 17:53:12 2000 +0100
@@ -103,7 +103,7 @@
 
 fun rbeta th = 
   case Dcterm.strip_comb (cconcl th)
-   of (eeq,[l,r]) => transitive th (beta_conversion r)
+   of (eeq,[l,r]) => transitive th (beta_conversion false r)
     | _ => raise RULES_ERR{func="rbeta", mesg =""};
 
 (*----------------------------------------------------------------------------
@@ -452,10 +452,10 @@
 fun SUBS thl = 
    rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl); (* FIXME do not handle _ !!! *)
 
-local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None))
+local fun rew_conv mss = MetaSimplifier.rewrite_cterm (true,false,false) (K(K None)) mss
 in
 fun simpl_conv ss thl ctm = 
- rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
+ rew_conv (MetaSimplifier.mss_of (#simps (MetaSimplifier.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
  RS meta_eq_to_obj_eq
 end;
 
@@ -562,7 +562,7 @@
  *---------------------------------------------------------------------------*)
 
 fun list_beta_conv tm =
-  let fun rbeta th = transitive th (beta_conversion(#2(D.dest_eq(cconcl th))))
+  let fun rbeta th = transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))
       fun iter [] = reflexive tm
         | iter (v::rst) = rbeta (combination(iter rst) (reflexive v))
   in iter  end;
@@ -713,7 +713,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 = Thm.rewrite_cterm (false,true,false) mss' (prover used) lhs
+                     val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) mss' lhs
                        handle _ => reflexive lhs (* FIXME do not handle _ !!! *)
                      val dummy = print_thms "proven:" [lhs_eq_lhs1]
                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
@@ -735,7 +735,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 = Thm.rewrite_cterm (false,true,false) mss' (prover used') Q1
+                  val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1
                                 handle _ => reflexive Q1 (* FIXME do not handle _ !!! *)
                   val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
@@ -760,8 +760,8 @@
                  let val tych = cterm_of sign
                      val ants1 = map tych ants
                      val mss' = add_prems(mss, map ASSUME ants1)
-                     val Q_eeq_Q1 = Thm.rewrite_cterm
-                        (false,true,false) mss' (prover used') (tych Q)
+                     val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
+                        (false,true,false) (prover used') mss' (tych Q)
                       handle _ => reflexive (tych Q) (* FIXME do not handle _ !!! *)
                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
                      val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
@@ -831,8 +831,8 @@
     end
     val ctm = cprop_of th
     val names = add_term_names (term_of ctm, [])
-    val th1 = Thm.rewrite_cterm(false,true,false) 
-      (add_congs(mss_of [cut_lemma'], congs)) (prover names) ctm
+    val th1 = MetaSimplifier.rewrite_cterm(false,true,false) 
+      (prover names) (add_congs(mss_of [cut_lemma'], congs)) ctm
     val th2 = equal_elim th1 th
  in
  (th2, filter (not o restricted) (!tc_list))
diff -r 5b33e732e459 -r 42e6b8502d52 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Tue Nov 07 17:52:12 2000 +0100
+++ b/src/Pure/Interface/proof_general.ML	Tue Nov 07 17:53:12 2000 +0100
@@ -145,7 +145,7 @@
 (* prepare theory context *)
 
 val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
-val update_thy_only = setmp Thm.trace_simp false ThyInfo.update_thy_only;
+val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
 
 fun which_context () =
   (case Context.get_context () of
diff -r 5b33e732e459 -r 42e6b8502d52 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Nov 07 17:52:12 2000 +0100
+++ b/src/Pure/Isar/method.ML	Tue Nov 07 17:53:12 2000 +0100
@@ -279,7 +279,7 @@
 (* atomize meta-connectives *)
 
 fun rewrite_goal_tac rews =
-  Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews);
+  Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
 
 fun atomize_tac rews =
   let val rew_tac = rewrite_goal_tac rews in