diff -r 33f00ce23e63 -r 91281e9472d8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Aug 02 11:32:23 2012 +0200
+++ b/src/Pure/Pure.thy	Thu Aug 02 12:36:54 2012 +0200
@@ -80,8 +80,15 @@
   and "use_thy" "remove_thy" "kill_thy" :: control
   and "display_drafts" "print_drafts" "pr" :: diag
   and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+  and "welcome" :: diag
+  and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
   and "end" :: thy_end % "theory"
-  uses "Isar/isar_syn.ML"
+  and "realizers" "realizability" "extract_type" "extract" :: thy_decl
+  and "find_theorems" "find_consts" :: diag
+  uses
+    "Isar/isar_syn.ML"
+    "Tools/find_theorems.ML"
+    "Tools/find_consts.ML"
 begin
 
 section {* Further content for the Pure theory *}