diff -r 2751f7f31be2 -r 51425cbe8ce9 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Aug 15 19:11:11 2015 +0200
+++ b/src/Pure/ROOT.ML	Sat Aug 15 19:42:35 2015 +0200
@@ -344,9 +344,10 @@
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
 toplevel_pp ["Position", "T"] "Pretty.position";
 toplevel_pp ["Binding", "binding"] "Binding.pp";
-toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
-toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
-toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
+toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory";
+toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory";
+toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory";
+toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory";
 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
 toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
@@ -364,9 +365,7 @@
 use "ML/ml_file.ML";
 Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
 Context.set_thread_data NONE;
-structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
-
-toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
+structure Pure = struct val thy = Thy_Info.pure_theory () end;
 
 
 (* ML toplevel commands *)