src/Pure/drule.ML

   val symmetric_fun     : thm -> thm
   val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_thm	: bool * bool * bool
                           -> (meta_simpset -> thm -> thm option)
                           -> meta_simpset -> thm -> thm
+  val rewrite_cterm	: bool * bool * bool
+                          -> (meta_simpset -> thm -> thm option)
+                          -> meta_simpset -> cterm -> thm
   val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_goal_rule	: bool* bool * bool
                           -> (meta_simpset -> thm -> thm option)
                           -> meta_simpset -> int -> thm -> thm
   val equal_abs_elim	: cterm  -> thm -> thm

 fun rewrite_rule_aux _ []   th = th
   | rewrite_rule_aux prover thms th =
       fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th;
 
 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
+fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover;
 
 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
 fun rewrite_goals_rule_aux _ []   th = th
   | rewrite_goals_rule_aux prover thms th =
       fconv_rule (goals_conv (K true) (rew_conv (true, true, false) prover