src/Pure/ROOT.ML
changeset 7938 e45599caee6c
parent 6783 9cf9c17d9e35
child 8538 e8ab6cd2e908
equal deleted inserted replaced
7937:82025fe607d3 7938:e45599caee6c
    79 
    79 
    80 val use = ThyInfo.use;
    80 val use = ThyInfo.use;
    81 val cd = File.cd o Path.unpack;
    81 val cd = File.cd o Path.unpack;
    82 
    82 
    83 print_depth 8;
    83 print_depth 8;
    84 (*ml_prompts "ML> " "ML# ";*)
    84 ml_prompts "ML> " "ML# ";
    85 
    85 
    86 Session.finish ();
    86 Session.finish ();