# 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'