src/Pure/simplifier.ML
changeset 32738 15bb09ca0378
parent 32148 253f6808dabe
child 32786 f1ac4b515af9
     1.1 --- a/src/Pure/simplifier.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    include BASIC_SIMPLIFIER
     1.5    val pretty_ss: Proof.context -> simpset -> Pretty.T
     1.6    val clear_ss: simpset -> simpset
     1.7 -  val debug_bounds: bool ref
     1.8 +  val debug_bounds: bool Unsynchronized.ref
     1.9    val inherit_context: simpset -> simpset -> simpset
    1.10    val the_context: simpset -> Proof.context
    1.11    val context: Proof.context -> simpset -> simpset
    1.12 @@ -424,5 +424,5 @@
    1.13  
    1.14  end;
    1.15  
    1.16 -structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
    1.17 -open BasicSimplifier;
    1.18 +structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
    1.19 +open Basic_Simplifier;