src/HOL/Tools/Lifting/lifting_setup.ML

         |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
           [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
         |> pair NONE
   in
     lthy''
+      |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), 
+        [quot_thm])
       |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), 
         [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
       |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]), 
         [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
       |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),