# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267443055 -3600
# Node ID 1810b1ade437883b807ab6cf3504dbe8a2153a9d
# Parent  cafb74a131da7a78ddfd23d9377c91bd48d36c8b
export add_quotient_type.

diff -r cafb74a131da -r 1810b1ade437 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Mar 01 09:47:44 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Mar 01 12:30:55 2010 +0100
@@ -7,6 +7,9 @@
 
 signature QUOTIENT_TYPE =
 sig
+  val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm
+    -> Proof.context -> (thm * thm) * local_theory
+
   val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
     -> Proof.context -> Proof.state
 
@@ -128,7 +131,7 @@
 
 
 (* main function for constructing a quotient type *)
-fun mk_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
+fun add_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
   (* generates the typedef *)
   val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
@@ -264,7 +267,7 @@
   val goals = map (mk_goal o snd) quot_list
 
   fun after_qed thms lthy =
-    fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd
+    fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
 in
   theorem after_qed goals lthy
 end