author | wenzelm |
Sun, 15 Apr 2007 14:31:52 +0200 | |
changeset 22694 | 077ce0e019fa |
parent 22693 | fb5e080fa82b |
child 22695 | 17073e9b94f2 |
src/Pure/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/ROOT.ML Sun Apr 15 14:31:51 2007 +0200 +++ b/src/Pure/ROOT.ML Sun Apr 15 14:31:52 2007 +0200 @@ -29,6 +29,7 @@ use "type.ML"; use "context.ML"; use "compress.ML"; +use "type_infer.ML"; (*inner syntax module*) use "Syntax/lexicon.ML"; @@ -50,7 +51,6 @@ structure Mixfix = Hidden; structure Printer = Hidden; -use "type_infer.ML"; use "General/ml_syntax.ML"; (*core of tactical proof system*)