src/HOL/Tools/Lifting/lifting_def.ML
changeset 47373 3c31e6f1b3bd
parent 47361 87c0eaf04bad
child 47379 075d22b3a32f
equal deleted inserted replaced
47372:9ab4e22dac7b 47373:3c31e6f1b3bd
   184 
   184 
   185     val lhs_name = Binding.name_of (#1 var)
   185     val lhs_name = Binding.name_of (#1 var)
   186     val rsp_thm_name = qualify lhs_name "rsp"
   186     val rsp_thm_name = qualify lhs_name "rsp"
   187     val code_eqn_thm_name = qualify lhs_name "rep_eq"
   187     val code_eqn_thm_name = qualify lhs_name "rep_eq"
   188     val transfer_thm_name = qualify lhs_name "transfer"
   188     val transfer_thm_name = qualify lhs_name "transfer"
       
   189     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   189   in
   190   in
   190     lthy'
   191     lthy'
   191       |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
   192       |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
   192       |> (snd oo Local_Theory.note) ((transfer_thm_name, []), [transfer_thm])
   193       |> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm])
   193       |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
   194       |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
   194   end
   195   end
   195 
   196 
   196 fun mk_readable_rsp_thm_eq tm lthy =
   197 fun mk_readable_rsp_thm_eq tm lthy =
   197   let
   198   let