polyml_as_definition does not require explicit dependencies on external ML files
authorhaftmann
Wed, 03 Nov 2010 10:44:53 +0100
changeset 40320 abc52faa7761
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
--- a/src/Tools/Code/code_runtime.ML	Wed Nov 03 08:29:32 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Nov 03 10:44:53 2010 +0100
@@ -418,8 +418,7 @@
       (0, Path.implode filepath) false (File.read filepath);
     val thy'' = (Context.the_theory o the) (Context.thread_data ());
     val names = Loaded_Values.get thy'';
-    val thy''' = Thy_Load.provide_file filepath thy'';
-  in (names, thy''') end;
+  in (names, thy'') end;
 
 end;