changeset 29315 | b074c05f00ad |
parent 29308 | ddf7fad4448c |
child 29339 | d8df32ab1172 |
--- a/src/Pure/Isar/ROOT.ML Fri Jan 02 16:21:10 2009 +0100 +++ b/src/Pure/Isar/ROOT.ML Fri Jan 02 16:21:47 2009 +0100 @@ -80,7 +80,7 @@ (*theory syntax*) use "../Thy/term_style.ML"; use "../Thy/thy_output.ML"; -use "../Thy/thy_edit.ML"; +use "../Thy/thy_syntax.ML"; use "../old_goals.ML"; use "outer_syntax.ML"; use "../Thy/thy_info.ML";