suppress slightly odd completions of "real";

--- a/src/Pure/Pure.thy	Tue Apr 29 22:50:55 2014 +0200
+++ b/src/Pure/Pure.thy	Tue Apr 29 22:52:15 2014 +0200
@@ -97,7 +97,9 @@
   and "welcome" :: diag
   and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
   and "end" :: thy_end % "theory"
-  and "realizers" "realizability" "extract_type" "extract" :: thy_decl
+  and "realizers" :: thy_decl == ""
+  and "realizability" :: thy_decl == ""
+  and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
   and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
     "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"