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