src/Pure/ROOT.ML
changeset 48927 ef462b5558eb
parent 48879 cb5cdbb645cd
child 48990 12814717c95c
     1.1 --- a/src/Pure/ROOT.ML	Sun Aug 26 10:20:26 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Sun Aug 26 21:46:50 2012 +0200
     1.3 @@ -306,7 +306,7 @@
     1.4  (* the Pure theory *)
     1.5  
     1.6  use "pure_syn.ML";
     1.7 -Thy_Info.use_thy "Pure";
     1.8 +Thy_Info.use_thy ("Pure", Position.none);
     1.9  Context.set_thread_data NONE;
    1.10  structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    1.11  
    1.12 @@ -341,8 +341,8 @@
    1.13  
    1.14  fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    1.15  
    1.16 -fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
    1.17 -fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
    1.18 +fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
    1.19 +val use_thy = use_thys o single;
    1.20  
    1.21  val cd = File.cd o Path.explode;
    1.22