src/Pure/Thy/thy_info.ML
changeset 62876 507c90523113
parent 62847 1bd1d8492931
child 62891 7a11ea5c9626
--- a/src/Pure/Thy/thy_info.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -260,7 +260,7 @@
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
       Resources.load_thy document symbols last_timing update_time dir header text_pos text
-        (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
+        (if name = Context.PureN then [Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
   in
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}