# HG changeset patch
# User wenzelm
# Date 1434375218 -7200
# Node ID aa4989ee74a5d7feb6c601c9b7a33afc5394cfc9
# Parent  98ee8635435416c42df37b7352a6b8027054da31
tuned;

diff -r 98ee86354354 -r aa4989ee74a5 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- 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) =