src/HOL/Tools/Lifting/lifting_def_code_dt.ML

     error error_msg
   end
 
 fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
   let
-    val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
+    val (_, ctxt') = Proof_Context.read_var raw_var ctxt
     val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
     val error_msg = cat_lines
        ["Lifting failed for the following term:",
         Pretty.string_of (Pretty.block
          [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),

     end
 
 fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
   let
     val config = evaluate_params params
-    val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy
+    val ((binding, SOME qty, mx), lthy) = Proof_Context.read_var raw_var lthy
     val var = (binding, mx)
     val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
     val par_thms = Attrib.eval_thms lthy par_xthms
     val (goal, after_qed) = prepare_lift_def (add_lift_def_code_dt config) var qty rhs par_thms lthy
     val (goal, after_qed) =