--- a/src/Tools/Metis/src/PortableIsabelle.sml Mon Sep 13 16:44:20 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* ========================================================================= *)
-(* Isabelle ML SPECIFIC FUNCTIONS *)
-(* ========================================================================= *)
-
-structure Portable :> Portable =
-struct
-
-(* ------------------------------------------------------------------------- *)
-(* The ML implementation. *)
-(* ------------------------------------------------------------------------- *)
-
-val ml = ml_system;
-
-(* ------------------------------------------------------------------------- *)
-(* Pointer equality using the run-time system. *)
-(* ------------------------------------------------------------------------- *)
-
-val pointerEqual = pointer_eq;
-
-(* ------------------------------------------------------------------------- *)
-(* Timing function applications a la Mosml.time. *)
-(* ------------------------------------------------------------------------- *)
-
-val time = timeap;
-
-(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-fun CRITICAL e = NAMED_CRITICAL "metis" e;
-
-(* ------------------------------------------------------------------------- *)
-(* Generating random values. *)
-(* ------------------------------------------------------------------------- *)
-
-val randomWord = Random_Word.next_word;
-val randomBool = Random_Word.next_bool;
-fun randomInt n = Random_Word.next_int 0 (n - 1);
-val randomReal = Random_Word.next_real;
-
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Quotations a la Moscow ML. *)
-(* ------------------------------------------------------------------------- *)
-
-datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a;