--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 05 10:48:46 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 05 12:18:06 2012 +0200
@@ -186,10 +186,11 @@
val rsp_thm_name = qualify lhs_name "rsp"
val code_eqn_thm_name = qualify lhs_name "rep_eq"
val transfer_thm_name = qualify lhs_name "transfer"
+ val transfer_attr = Attrib.internal (K Transfer.transfer_add)
in
lthy'
|> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
- |> (snd oo Local_Theory.note) ((transfer_thm_name, []), [transfer_thm])
+ |> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm])
|> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
end