src/Pure/ML-Systems/no_multithreading.ML
changeset 23921 947152add153
child 23946 4fbb1ff12337
equal deleted inserted replaced
23920:4288dc7dc248 23921:947152add153
       
     1 (*  Title:      Pure/ML-Systems/no_multithreading.ML
       
     2     ID:         $Id$
       
     3     Author:     Makarius
       
     4 
       
     5 Compatibility file for ML systems without multithreading.
       
     6 *)
       
     7 
       
     8 (* critical section *)
       
     9 
       
    10 fun CRITICAL e = e ();