src/Pure/ML-Systems/smlnj.ML
changeset 16528 25a7459d4d4a
parent 16502 5a56e59526a5
child 16542 1259088dc448
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Jun 22 11:09:14 2005 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jun 22 11:20:45 2005 +0200
     1.3 @@ -13,9 +13,13 @@
     1.4  
     1.5  (* low-level pointer equality *)
     1.6  
     1.7 -(*proper implementation available?*)
     1.8 +(*proper implementation available? This declaration may get overridden below.*)
     1.9  fun pointer_eq (x:''a, y) = false;
    1.10  
    1.11 +(case #version_id (Compiler.version) of
    1.12 +  [110, x] => if x >= 49 then use "ML-Systems/smlnj-ptreql.ML" else ()
    1.13 +| _ => ());
    1.14 +
    1.15  
    1.16  (* restore old-style character / string functions *)
    1.17