src/Tools/Metis/src/Random.sml
changeset 39429 126b879df319
parent 39426 c551ce5f614a
--- a/src/Tools/Metis/src/Random.sml	Wed Sep 15 18:52:37 2010 +0200
+++ b/src/Tools/Metis/src/Random.sml	Wed Sep 15 19:22:34 2010 +0200
@@ -9,9 +9,6 @@
 structure Random :> Random =
 struct
 
-(* MODIFIED by Jasmin Blanchette *)
-fun CRITICAL e = NAMED_CRITICAL "metis" e;
-
 (* random words: 0w0 <= result <= max_word *)
 
 (*minimum length of unboxed words on all supported ML platforms*)