1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Oct 15 00:08:02 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Oct 15 00:08:03 2005 +0200
     1.3 @@ -433,6 +433,12 @@
     1.4          --| P.$$$ "where") [] -- statement
     1.5        >> (Toplevel.print oo (Toplevel.proof' o (ProofHistory.apply oo uncurry Obtain.obtain))));
     1.6  
     1.7 +val guessP =
     1.8 +  OuterSyntax.command "guess" "wild guessing (unstructured)"
     1.9 +    (K.tag_proof K.prf_asm_goal)
    1.10 +    (P.and_list (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
    1.11 +      >> (Toplevel.print oo (Toplevel.proof' o (ProofHistory.applys oo Obtain.guess))));
    1.12 +
    1.13  val letP =
    1.14    OuterSyntax.command "let" "bind text variables"
    1.15      (K.tag_proof K.prf_decl)
    1.16 @@ -848,8 +854,8 @@
    1.17    print_ast_translationP, token_translationP, oracleP, localeP,
    1.18    (*proof commands*)
    1.19    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
    1.20 -  assumeP, presumeP, defP, obtainP, letP, caseP, thenP, fromP, withP,
    1.21 -  noteP, usingP, beginP, endP, nextP, qedP, terminal_proofP,
    1.22 +  assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
    1.23 +  withP, noteP, usingP, beginP, endP, nextP, qedP, terminal_proofP,
    1.24    default_proofP, immediate_proofP, done_proofP, skip_proofP,
    1.25    forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
    1.26    finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,