src/Pure/ROOT.ML
changeset 62662 291cc01f56f5
parent 62661 c23ff2f45a18
child 62665 a78ce0c6e191
     1.1 --- a/src/Pure/ROOT.ML	Thu Mar 17 13:44:18 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Mar 17 16:56:44 2016 +0100
     1.3 @@ -69,10 +69,6 @@
     1.4  PolyML.Compiler.printInAlphabeticalOrder := false;
     1.5  PolyML.Compiler.maxInlineSize := 80;
     1.6  
     1.7 -fun ml_make_string struct_name =
     1.8 -  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
     1.9 -    struct_name ^ ".ML_print_depth ()))))))";
    1.10 -
    1.11  
    1.12  (* ML debugger *)
    1.13