src/Pure/ML-Systems/polyml_common.ML

 (* prompts *)
 
 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
   fun get_print_depth () = ! depth;
   fun print_depth n = (depth := n; PolyML.print_depth n);