src/Pure/raw_simplifier.ML

   val prems_of: Proof.context -> thm list
   val add_simp: thm -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
   val flip_simp: thm -> Proof.context -> Proof.context
   val init_simpset: thm list -> Proof.context -> Proof.context
+  val mk_cong: Proof.context -> thm -> thm
   val add_eqcong: thm -> Proof.context -> Proof.context
   val del_eqcong: thm -> Proof.context -> Proof.context
   val add_cong: thm -> Proof.context -> Proof.context
   val del_cong: thm -> Proof.context -> Proof.context
   val mksimps: Proof.context -> thm -> thm list

   in
     f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
     is_full_cong_prems prems (xs ~~ ys)
   end;
 
+in
+
 fun mk_cong ctxt = #mk_cong (get_mk_rews ctxt) ctxt;
-
-in
 
 fun add_eqcong thm ctxt = ctxt |> map_simpset2
   (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)