polyml_as_definition does not require explicit dependencies on external ML files
authorhaftmann
Wed Nov 03 10:44:53 2010 +0100 (2010-11-03)
changeset 40320abc52faa7761
parent 40311 994e784ca17a
child 40330 3b7f570723f9
child 40346 58af2b8327b7
polyml_as_definition does not require explicit dependencies on external ML files
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Wed Nov 03 08:29:32 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Nov 03 10:44:53 2010 +0100
     1.3 @@ -418,8 +418,7 @@
     1.4        (0, Path.implode filepath) false (File.read filepath);
     1.5      val thy'' = (Context.the_theory o the) (Context.thread_data ());
     1.6      val names = Loaded_Values.get thy'';
     1.7 -    val thy''' = Thy_Load.provide_file filepath thy'';
     1.8 -  in (names, thy''') end;
     1.9 +  in (names, thy'') end;
    1.10  
    1.11  end;
    1.12