# HG changeset patch
# User wenzelm
# Date 1131652640 -3600
# Node ID dd287c773455d1a1f6ca1abc5c880867baab3c95
# Parent  c6899e23b5ff45e6af802536dd009738a705950f
guess: Toplevel.proof;

diff -r c6899e23b5ff -r dd287c773455 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 10 20:57:19 2005 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 10 20:57:20 2005 +0100
@@ -436,7 +436,7 @@
   OuterSyntax.command "guess" "wild guessing (unstructured)"
     (K.tag_proof K.prf_asm_goal)
     (P.and_list (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
-      >> (Toplevel.print oo (Toplevel.proofs' o Obtain.guess)));
+      >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
 
 val letP =
   OuterSyntax.command "let" "bind text variables"