diff -r 0562a0a5bb93 -r d44c87988a24 src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Sun Nov 28 20:12:22 2010 +0100 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Sun Nov 28 20:36:45 2010 +0100 @@ -140,17 +140,17 @@ else (); fun apply_fix (a, b) = - (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); + (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b)); fun apply_type (a, b) = - (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b)); + (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space)); fun apply_sig (a, b) = - (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); + (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space)); fun apply_struct (a, b) = - (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); + (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space)); fun apply_funct (a, b) = - (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b)); + (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space)); fun apply_val (a, b) = - (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b)); + (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space)); in List.app apply_fix fixes; List.app apply_type types;