src/Pure/ML-Systems/smlnj.ML
changeset 41411 3bcc3b9e1020
parent 40748 591b6778d076
child 42012 2c3fe3cbebae
equal deleted inserted replaced
41410:3d99be274463 41411:3bcc3b9e1020
    23 
    23 
    24 (*low-level pointer equality*)
    24 (*low-level pointer equality*)
    25 
    25 
    26 CM.autoload "$smlnj/init/init.cmi";
    26 CM.autoload "$smlnj/init/init.cmi";
    27 val pointer_eq = InlineT.ptreql;
    27 val pointer_eq = InlineT.ptreql;
       
    28 
       
    29 fun share_common_data () = ();
    28 
    30 
    29 
    31 
    30 (* restore old-style character / string functions *)
    32 (* restore old-style character / string functions *)
    31 
    33 
    32 val ord = mk_int o SML90.ord;
    34 val ord = mk_int o SML90.ord;