--- 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;