src/Pure/ROOT.ML
changeset 37146 f652333bbf8e
parent 37145 01aa36932739
child 37216 3165bc303f66
     1.1 --- a/src/Pure/ROOT.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -310,6 +310,7 @@
     1.4  structure OuterSyntax = Outer_Syntax;
     1.5  structure SpecParse = Parse_Spec;
     1.6  structure TypeInfer = Type_Infer;
     1.7 +structure PrintMode = Print_Mode;
     1.8  
     1.9  end;
    1.10