diff -r d659a12f9b7f -r 8451eddc4d67 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Oct 31 15:08:51 2014 +0100
+++ b/src/Pure/Pure.thy	Fri Oct 31 15:15:10 2014 +0100
@@ -79,21 +79,20 @@
   and "also" "moreover" :: prf_decl % "proof"
   and "finally" "ultimately" :: prf_chain % "proof"
   and "back" :: prf_script % "proof"
-  and "Isabelle.command" :: control
   and "help" "print_commands" "print_options" "print_context"
     "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
     "print_theorems" "print_locales" "print_classes" "print_locale"
     "print_interps" "print_dependencies" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     "print_antiquotations" "print_ML_antiquotations" "thy_deps"
-    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
+    "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
     "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
   and "use_thy" "remove_thy" "kill_thy" :: control
-  and "display_drafts" "print_state" "pr" :: diag
-  and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+  and "display_drafts" "print_state" :: diag
+  and "commit" "quit" "exit" :: control
   and "welcome" :: diag
-  and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
+  and "init_toplevel" "linear_undo" "undo" "undos_proof" "kill" :: control
   and "end" :: thy_end % "theory"
   and "realizers" :: thy_decl == ""
   and "realizability" :: thy_decl == ""