TFL/rules.sml

        val ctm2_eq = reflexive ctm2
        val ctm1_eq = reflexive ctm1
    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
  *---------------------------------------------------------------------------*)
 fun INST_TYPE blist thm = 

           end handle _ => None
     in
     (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
  (th2, filter (not o restricted) (!tc_list))
  end;