--- 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"