author | wenzelm |
Sat, 29 May 2004 15:00:25 +0200 | |
changeset 14823 | ebb8499d0fd2 |
parent 14822 | c5fcde6324a2 |
child 14824 | 336ade035a34 |
src/Pure/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/ROOT.ML Sat May 29 15:00:14 2004 +0200 +++ b/src/Pure/ROOT.ML Sat May 29 15:00:25 2004 +0200 @@ -12,9 +12,6 @@ print_depth 10; -(*global flags*) -val print_mode = ref ([]: string list); - (*fake hiding of private structures*) structure Hidden = struct end; @@ -24,6 +21,7 @@ (*fundamental structures*) use "term.ML"; +use "General/pretty.ML"; use "sorts.ML"; use "type.ML";