[isabelle] antiquotation for the current goal



Dear Isabelle Users,
for debugging purposes I would like to have an antiquotation that would give me a current goal as a term. For example:

lemma "A ∧ B"
apply (rule conjI)

ML_prf{*
@{goal} (* would output val it = Const ("HOL.Trueprop", "bool ⇒ prop") $ Free ("A", "bool"): term *)
*}

I found that there is @{Isar.goal} but that gives me only an error message "No goal present". I also tried some ML like "Toplevel.proof_of (Toplevel.toplevel)" but that gives me a similar result "exception UNDEF raised (line 168 of "Isar/toplevel.ML")".

Is there a way how to have such an antiquotation?

Thanks for your answers.

Best,
Ondrej




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.