# HG changeset patch
# User wenzelm
# Date 1377526400 -7200
# Node ID 9745b7d4cc795b1a58beb8bcf2cb908ac6856096
# Parent  5d2fe75c6306e2af720a1cf80e535959ee8bd620
prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;

diff -r 5d2fe75c6306 -r 9745b7d4cc79 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Aug 26 15:57:09 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Aug 26 16:13:20 2013 +0200
@@ -406,7 +406,7 @@
     val absrep_trm =  quot_thm_abs quot_thm
     val rty_forced = (domain_type o fastype_of) absrep_trm
     val forced_rhs = force_rty_type lthy rty_forced rhs
-    val lhs = Free (Binding.print (#1 var), qty)
+    val lhs = Free (Binding.name_of (#1 var), qty)
     val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
     val (_, prop') = Local_Defs.cert_def lthy prop
     val (_, newrhs) = Local_Defs.abs_def prop'