updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)

(* Could go in the programming tutorial *)

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