changeset 2 | c67f44be880f |
parent 0 | a5a9c433f639 |
child 19 | 929ad32d63fc |
--- a/src/Pure/ROOT.ML Thu Sep 16 14:21:44 1993 +0200 +++ b/src/Pure/ROOT.ML Thu Sep 16 16:25:32 1993 +0200 @@ -28,11 +28,6 @@ use "ROOT.ML"; cd ".."; -(* Theory parser *) -cd "Thy"; -use "ROOT.ML"; -cd ".."; - print_depth 1; use "type.ML"; use "sign.ML"; @@ -69,3 +64,9 @@ open Basic_Syntax Thm Drule Tactical Tactic Goals; structure Pure = struct val thy = pure_thy end; + +(* Theory parser *) +cd "Thy"; +use "ROOT.ML"; +cd ".."; +