export of proper information in the ML-interface of the quotient package

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jun 24 11:08:21 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jun 24 12:33:51 2010 +0100
@@ -7,13 +7,13 @@
 signature QUOTIENT_DEF =
 sig
   val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
-    local_theory -> (term * thm) * local_theory
+    local_theory -> Quotient_Info.qconsts_info * local_theory
 
   val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
-    local_theory -> (term * thm) * local_theory
+    local_theory -> Quotient_Info.qconsts_info * local_theory
 
   val quotient_lift_const: typ list -> string * term -> local_theory ->
-    (term * thm) * local_theory
+    Quotient_Info.qconsts_info * local_theory
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -45,7 +45,7 @@
   val pos = Position.str_of (Binding.pos_of bind)
 in
   error ("Head of quotient_definition " ^ 
-    (quote str) ^ " differs from declaration " ^ name ^ pos)
+    quote str ^ " differs from declaration " ^ name ^ pos)
 end
 
 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
@@ -69,12 +69,14 @@
   val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
 
   (* data storage *)
-  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
+  val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+
+  fun qcinfo phi = transform_qconsts phi qconst_data
   fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
   val lthy'' = Local_Theory.declaration true
                  (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
 in
-  ((trm, thm), lthy'')
+  (qconst_data, lthy'')
 end
 
 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =

--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jun 24 11:08:21 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jun 24 12:33:51 2010 +0100
@@ -84,7 +84,7 @@
 *)
 fun mk_mapfun ctxt vs rty =
 let
-  val vs' = map (mk_Free) vs
+  val vs' = map mk_Free vs
 
   fun mk_mapfun_aux rty =
     case rty of
@@ -103,7 +103,7 @@
 let
   val thy = ProofContext.theory_of ctxt
   val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+  val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn
 in
   (#rtyp qdata, #qtyp qdata)
 end

--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Jun 24 11:08:21 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Jun 24 12:33:51 2010 +0100
@@ -8,7 +8,7 @@
 signature QUOTIENT_TYPE =
 sig
   val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
-    -> Proof.context -> (thm * thm) * local_theory
+    -> Proof.context -> Quotient_Info.quotdata_info * local_theory
 
   val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
     -> Proof.context -> Proof.state
@@ -32,11 +32,8 @@
 end
 
 fun note (name, thm, attrs) lthy =
-let
-  val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
-in
-  (thm', lthy')
-end
+  Local_Theory.note ((name, attrs), [thm]) lthy |> snd
+
 
 fun intern_attr at = Attrib.internal (K at)
 
@@ -64,7 +61,7 @@
     |> map Free
 in
   lambda c (HOLogic.exists_const rty $
-     lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x))))))
+     lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
 end
 
 
@@ -139,7 +136,10 @@
 (* main function for constructing a quotient type *)
 fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
 let
-  val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp}
+  val part_equiv = 
+    if partial 
+    then equiv_thm 
+    else equiv_thm RS @{thm equivp_implies_part_equivp}
 
   (* generates the typedef *)
   val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
@@ -173,15 +173,17 @@
   (* name equivalence theorem *)
   val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
 
-  (* storing the quot-info *)
-  fun qinfo phi = transform_quotdata phi
-    {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
-  val lthy4 = Local_Theory.declaration true
-    (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3
+  (* storing the quotdata *)
+  val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
+
+  fun qinfo phi = transform_quotdata phi quotdata
+
+  val lthy4 = lthy3
+     |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
+     |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
+     |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
 in
-  lthy4
-  |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
-  ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
+  (quotdata, lthy4)
 end
 
 
@@ -253,6 +255,7 @@
  - its free type variables (first argument)
  - its mixfix annotation
  - the type to be quotient
+ - the partial flag (a boolean)
  - the relation according to which the type is quotient
 
  it opens a proof-state in which one has to show that the
@@ -268,7 +271,8 @@
   fun mk_goal (rty, rel, partial) =
   let
     val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
-    val const = if partial then @{const_name part_equivp} else @{const_name equivp}
+    val const = 
+      if partial then @{const_name part_equivp} else @{const_name equivp}
   in
     HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
   end