diff -r ef65d5ee60cf -r 47b23c582127 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Sep 02 11:03:02 2013 +0200
+++ b/src/Pure/Pure.thy	Mon Sep 02 16:10:26 2013 +0200
@@ -60,7 +60,8 @@
   and "then" "from" "with" :: prf_chain % "proof"
   and "note" "using" "unfolding" :: prf_decl % "proof"
   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
-  and "obtain" "guess" :: prf_asm_goal % "proof"
+  and "obtain" :: prf_asm_goal % "proof"
+  and "guess" :: prf_asm_goal_script % "proof"
   and "let" "write" :: prf_decl % "proof"
   and "case" :: prf_asm % "proof"
   and "{" :: prf_open % "proof"