src/HOL/Rat.thy

   uminus_rat.transfer times_rat.transfer inverse_rat.transfer
   positive.transfer of_rat.transfer
 
 text {* De-register @{text "rat"} as a quotient type: *}
 
-setup {* Context.theory_map (Lifting_Info.update_quotients @{type_name rat}
-  {quot_thm = @{thm identity_quotient [where 'a=rat]}}) *}
-
-end
+declare Quotient_rat[quot_del]
+
+end