src/Pure/ML-Systems/polyml_common.ML
changeset 30625 d53d1a16d5ee
parent 30619 0226c07352db
child 30672 beaadd5af500
--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -74,13 +74,8 @@
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
+(* print depth *)
 
-fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
-  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
-    fn () => brk (99999, 0), en);
-
-(*print depth*)
 local
   val depth = ref 10;
 in