src/Pure/ML-Systems/polyml-5.1.ML
changeset 29638 1f8f3d26a2cf
parent 29564 f8b933a62151
child 30627 fb9e73c01603
     1.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 00:42:12 2009 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 12:59:22 2009 +0100
     1.3 @@ -8,3 +8,6 @@
     1.4  use "ML-Systems/polyml_old_compiler5.ML";
     1.5  
     1.6  val pointer_eq = PolyML.pointerEq;
     1.7 +
     1.8 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
     1.9 +