# HG changeset patch
# User wenzelm
# Date 1460312139 -7200
# Node ID ba10c4e226cf50eb4094d4aa092a68e2cd18ecf7
# Parent  5612ec9f0f494637712105ea6962f4fbcbe09888
tuned;

diff -r 5612ec9f0f49 -r ba10c4e226cf src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Apr 10 18:41:49 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Apr 10 20:15:39 2016 +0200
@@ -103,7 +103,7 @@
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
-fun pure_theory () = get_theory "Pure";
+fun pure_theory () = get_theory Context.PureN;
 
 val get_imports = Resources.imports_of o get_theory;