changeset 14823 | ebb8499d0fd2 |
parent 14781 | 2be804d1dda9 |
child 15006 | 107e4dfd3b96 |
--- 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";