--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Mon Jun 15 14:10:41 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Mon Jun 15 15:33:38 2015 +0200
@@ -737,7 +737,7 @@
fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
let
val (_, ctxt') = Proof_Context.read_var raw_var ctxt
- val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
+ val rhs = Syntax.read_term ctxt' rhs_raw
val error_msg = cat_lines
["Lifting failed for the following term:",
Pretty.string_of (Pretty.block
@@ -761,7 +761,7 @@
val config = evaluate_params params
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 rhs = Syntax.read_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) =