TFL/rules.sml
changeset 7262 a05dc63ca29b
parent 6498 1ebbe18fe236
child 8882 9df44a4f1bf7
--- a/TFL/rules.sml	Wed Aug 18 18:10:48 1999 +0200
+++ b/TFL/rules.sml	Wed Aug 18 18:44:20 1999 +0200
@@ -46,6 +46,10 @@
    in equal_elim (transitive ctm2_eq ctm1_eq) thm
    end;
 
+fun rbeta th = 
+  case Dcterm.strip_comb (cconcl th)
+   of (eeq,[l,r]) => transitive th (beta_conversion r)
+    | _ => raise RULES_ERR{func="rbeta", mesg =""};
 
 (*----------------------------------------------------------------------------
  *        typ instantiation
@@ -772,7 +776,8 @@
     (if (is_cong thm) then cong_prover else restrict_prover) mss thm
     end
     val ctm = cprop_of th
-    val th1 = Thm.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