(* Could go in the programming tutorial *)+− +− ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}+−