Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_syn.ML
changeset 18150 dd287c773455
parent 18136 51385f358b53
child 18308 f18a54840629 
--- 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"
isabelle