src/HOL/Tools/Lifting/lifting_def.ML
changeset 53207 9745b7d4cc79
parent 53205 8d41170242cb
child 53651 ee90c67502c9
equal deleted inserted replaced
53206:5d2fe75c6306 53207:9745b7d4cc79
   404     val rty = fastype_of rhs
   404     val rty = fastype_of rhs
   405     val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
   405     val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
   406     val absrep_trm =  quot_thm_abs quot_thm
   406     val absrep_trm =  quot_thm_abs quot_thm
   407     val rty_forced = (domain_type o fastype_of) absrep_trm
   407     val rty_forced = (domain_type o fastype_of) absrep_trm
   408     val forced_rhs = force_rty_type lthy rty_forced rhs
   408     val forced_rhs = force_rty_type lthy rty_forced rhs
   409     val lhs = Free (Binding.print (#1 var), qty)
   409     val lhs = Free (Binding.name_of (#1 var), qty)
   410     val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
   410     val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
   411     val (_, prop') = Local_Defs.cert_def lthy prop
   411     val (_, prop') = Local_Defs.cert_def lthy prop
   412     val (_, newrhs) = Local_Defs.abs_def prop'
   412     val (_, newrhs) = Local_Defs.abs_def prop'
   413 
   413 
   414     val ((_, (_ , def_thm)), lthy') = 
   414     val ((_, (_ , def_thm)), lthy') =