src/HOL/Analysis/measurable.ML

   val get_dest : Context.generic -> thm list
   val get_cong : Context.generic -> thm list
 
   val measurable_tac : Proof.context -> thm list -> tactic
 
-  val simproc : Simplifier.proc
+  val proc : Simplifier.proc
 
   val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic
   val del_preprocessor : string -> Context.generic -> Context.generic
   val add_local_cong : thm -> Proof.context -> Proof.context
 
   val prepare_facts : Proof.context -> thm list -> (thm list * Proof.context)
-end ;
+end
 
 structure Measurable : MEASURABLE =
 struct
 
 type preprocessor = thm -> Proof.context -> thm list * Proof.context

       ORELSE' (CHANGED o sets_cong_tac)
       ORELSE' (K (debug_tac ctxt (K "backtrack") no_tac))
 
   in debug_tac ctxt (K "start") (REPEAT (single_step_tac 1)) end;
 
-fun simproc ctxt redex =
+fun proc ctxt redex =
   let
     val t = HOLogic.mk_Trueprop (Thm.term_of redex);
     fun tac {context = ctxt, prems = _ } =
       SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt));
   in \<^try>\<open>Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}\<close> end;