src/Pure/ML/ml_pervasive1.ML
changeset 62902 3c0f53eae166
parent 62889 99c7f31615c2
child 62923 3a122e1e352a
--- a/src/Pure/ML/ml_pervasive1.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_pervasive1.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -12,3 +12,5 @@
 Proofterm.proofs := 0;
 
 Context.put_generic_context NONE;
+
+val use = ML_file;