# HG changeset patch
# User wenzelm
# Date 947068922 -3600
# Node ID 226dcdc3c5f327fd3bbb372aa3539c2d87960519
# Parent  5a241706d9b3bb828316679bc9dfad731ca6d35b
ObtainFun;

diff -r 5a241706d9b3 -r 226dcdc3c5f3 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Wed Jan 05 11:41:38 2000 +0100
+++ b/src/Pure/Isar/ROOT.ML	Wed Jan 05 11:42:02 2000 +0100
@@ -19,7 +19,6 @@
 use "local_defs.ML";
 use "calculation.ML";
 use "skip_proof.ML";
-use "obtain.ML";
 
 (*outer syntax*)
 use "comment.ML";
@@ -30,7 +29,7 @@
 use "toplevel.ML";
 use "session.ML";
 
-(*theory operations*)
+(*theory and proof operations*)
 use "isar_thy.ML";
 use "isar_cmd.ML";
 
@@ -38,7 +37,8 @@
 use "outer_syntax.ML";
 use "isar_syn.ML";
 
-(*main ML interface*)
+(*main ML interfaces*)
+use "obtain.ML";
 use "isar.ML";
 
 structure PureIsar =
@@ -53,7 +53,6 @@
   structure LocalDefs = LocalDefs;
   structure Calculation = Calculation;
   structure SkipProof = SkipProof;
-  structure Obtain = Obtain;
   structure Comment = Comment;
   structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;