src/Pure/ROOT.ML
changeset 48927 ef462b5558eb
parent 48879 cb5cdbb645cd
child 48990 12814717c95c
--- a/src/Pure/ROOT.ML	Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/ROOT.ML	Sun Aug 26 21:46:50 2012 +0200
@@ -306,7 +306,7 @@
 (* the Pure theory *)
 
 use "pure_syn.ML";
-Thy_Info.use_thy "Pure";
+Thy_Info.use_thy ("Pure", Position.none);
 Context.set_thread_data NONE;
 structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
 
@@ -341,8 +341,8 @@
 
 fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
 
-fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
-fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
+fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
+val use_thy = use_thys o single;
 
 val cd = File.cd o Path.explode;