# HG changeset patch
# User kuncar
# Date 1334646735 -7200
# Node ID 4c949049cd78b08609d812a223eb8e6216a83f90
# Parent  0b9294e093dba47793b6c73e9e137d789848835d
note the Quotient theorem in quotient_type

diff -r 0b9294e093db -r 4c949049cd78 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Mon Apr 16 20:50:43 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Apr 17 09:12:15 2012 +0200
@@ -136,6 +136,9 @@
   let
     val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
     val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
+    val (rty, qty) = (dest_funT o fastype_of) abs_fun
+    val qty_name = (fst o dest_Type) qty
+    val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name) 
     val quot_thm = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
       Const (@{const_name equivp}, _) $ _ => 
         [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}
@@ -144,7 +147,9 @@
       | _ => error "unsupported equivalence theorem"
       )
   in
-    Lifting_Setup.setup_lifting_infr quot_thm equiv_thm lthy'
+    lthy'
+      |> Lifting_Setup.setup_lifting_infr quot_thm equiv_thm
+      |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
   end
 
 fun init_quotient_infr quot_thm equiv_thm lthy =