1 (* Could go in the programming tutorial *)

     2 

     3 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}