# HG changeset patch
# User huffman
# Date 1333621086 -7200
# Node ID 3c31e6f1b3bdfdca240ed02da114281214f5a154
# Parent  9ab4e22dac7b41e5c28b64303938bb1ee82271c9
lift_definition declares transfer_rule attribute

diff -r 9ab4e22dac7b -r 3c31e6f1b3bd src/HOL/Tools/Lifting/lifting_def.ML
--- 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