src/Pure/simplifier.ML

 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
   val pretty_ss: Proof.context -> simpset -> Pretty.T
   val clear_ss: simpset -> simpset
-  val debug_bounds: bool ref
+  val debug_bounds: bool Unsynchronized.ref
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
   val theory_context: theory  -> simpset -> simpset
   val simproc_i: theory -> string -> term list

     setmksimps mksimps
   end));
 
 end;
 
-structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
-open BasicSimplifier;
+structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
+open Basic_Simplifier;