--- a/src/Pure/Isar/ROOT.ML Sat Jun 28 22:58:49 2008 +0200 +++ b/src/Pure/Isar/ROOT.ML Sat Jun 28 23:52:43 2008 +0200 @@ -42,6 +42,7 @@ use "skip_proof.ML"; use "method.ML"; use "proof.ML"; +use "../ML/ml_thms.ML"; use "element.ML"; use "net_rules.ML";