# HG changeset patch
# User wenzelm
# Date 1398804735 -7200
# Node ID 32963b43a53842505474635bca43187d0e95e7d2
# Parent  9f84219715a7341788c788198c4d6570ac82ea8b
suppress slightly odd completions of "real";

diff -r 9f84219715a7 -r 32963b43a538 src/Pure/Pure.thy
--- 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"