guess: Toplevel.proof;
authorwenzelm
Thu Nov 10 20:57:20 2005 +0100 (2005-11-10)
changeset 18150dd287c773455
parent 18149 c6899e23b5ff
child 18151 32538cf750ca
guess: Toplevel.proof;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Nov 10 20:57:19 2005 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 10 20:57:20 2005 +0100
     1.3 @@ -436,7 +436,7 @@
     1.4    OuterSyntax.command "guess" "wild guessing (unstructured)"
     1.5      (K.tag_proof K.prf_asm_goal)
     1.6      (P.and_list (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
     1.7 -      >> (Toplevel.print oo (Toplevel.proofs' o Obtain.guess)));
     1.8 +      >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
     1.9  
    1.10  val letP =
    1.11    OuterSyntax.command "let" "bind text variables"