# HG changeset patch
# User wenzelm
# Date 1245093454 -7200
# Node ID ef30cd0e41e5f9f2c240c1f8fdfdc8a416c6b915
# Parent  98a3fd346270ca54c3fcbbe6a56253b7ea8c886a
override toplevel "use" functions last;

diff -r 98a3fd346270 -r ef30cd0e41e5 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Mon Jun 15 17:36:49 2009 +0200
+++ b/src/Pure/pure_setup.ML	Mon Jun 15 21:17:34 2009 +0200
@@ -4,15 +4,6 @@
 Pure theory and ML toplevel setup.
 *)
 
-(* ML toplevel use commands *)
-
-fun use name          = Toplevel.program (fn () => ThyInfo.use name);
-fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
-fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
-fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
-fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
-
-
 (* the Pure theories *)
 
 val theory = ThyInfo.get_theory;
@@ -49,6 +40,15 @@
 else ();
 
 
+(* ML toplevel use commands *)
+
+fun use name          = Toplevel.program (fn () => ThyInfo.use name);
+fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
+fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
+fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
+fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
+
+
 (* misc *)
 
 val cd = File.cd o Path.explode;