--- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu May 24 14:20:23 2012 +0200
@@ -103,8 +103,10 @@
fun quot_info phi = Lifting_Info.transform_quotients phi quotients
val lthy' = case maybe_reflp_thm of
SOME reflp_thm => lthy
- |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+ |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
[reflp_thm])
+ |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
+ [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
|> define_code_constr gen_code quot_thm
| NONE => lthy
|> define_abs_type gen_code quot_thm