--- 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))