src/Pure/Thy/read.ML
changeset 207 059e406442fd
parent 204 b9f087b42a44
child 212 b2cdb675ef44
equal deleted inserted replaced
206:0d624d1ba9cc 207:059e406442fd
   247 
   247 
   248     in if thy_uptodate andalso ml_uptodate then ()
   248     in if thy_uptodate andalso ml_uptodate then ()
   249        else
   249        else
   250        (
   250        (
   251          if thy_uptodate orelse thy_file = "" then ()
   251          if thy_uptodate orelse thy_file = "" then ()
   252          else (read_thy thyl thy_file;
   252          else (writeln ("Reading thy-file \"" ^ thyl ^ ".thy\"");
       
   253                read_thy thyl thy_file;
   253                use (out_name thyl)
   254                use (out_name thyl)
   254               );
   255               );
   255 
   256 
   256          if ml_file = "" then () 
   257          if ml_file = "" then () 
   257          else (writeln ("Reading ML-file \"" ^ thyl ^ ".ML\"");
   258          else (writeln ("Reading ML-file \"" ^ thyl ^ ".ML\"");