# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263509311 -3600
# Node ID fe7d27e197e5fdb78a1d3d3abd3e8b0c5e72531c
# Parent  e49c6b6f37f4c45a27f087824f24cd770c5151f9
tuned quotient_typ.ML

diff -r e49c6b6f37f4 -r fe7d27e197e5 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Thu Jan 14 23:17:21 2010 +0100
+++ b/Quot/quotient_typ.ML	Thu Jan 14 23:48:31 2010 +0100
@@ -74,9 +74,9 @@
 (* tactic to prove the Quot_Type theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
-  val rep_thm = (#Rep typedef_info) RS mem_def1
+  val rep_thm = #Rep typedef_info RS mem_def1
   val rep_inv = #Rep_inverse typedef_info
-  val abs_inv = mem_def2 RS (#Abs_inverse typedef_info)
+  val abs_inv = mem_def2 RS #Abs_inverse typedef_info
   val rep_inj = #Rep_inject typedef_info
 in
   (rtac @{thm Quot_Type.intro} THEN' 
@@ -88,7 +88,7 @@
 end
 
 
-(* proves the Quot_Type theorem *)
+(* proves the Quot_Type theorem for the new type *)
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
   val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT)
@@ -99,7 +99,7 @@
     (K (typedef_quot_type_tac equiv_thm typedef_info))
 end
 
-(* proves the quotient theorem *)
+(* proves the quotient theorem for the new type *)
 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
 let
   val quotient_const = Const (@{const_name "Quotient"}, dummyT)
@@ -117,7 +117,7 @@
 
 
 (* main function for constructing a quotient type *)
-fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
+fun mk_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
@@ -141,7 +141,7 @@
   val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
   val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
 
-  (* quot_type theorem - needed below *)
+  (* quot_type theorem *)
   val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3
 
   (* quotient theorem *)  
@@ -173,7 +173,7 @@
   val rel_frees = map fst (Term.add_frees rel [])
   val rel_vars = Term.add_vars rel []
   val rel_tvars = Term.add_tvars rel []
-  val qty_str = (Binding.str_of qty_name) ^ ": "
+  val qty_str = Binding.str_of qty_name ^ ": "
 
   val illegal_rel_vars =
     if null rel_vars andalso null rel_tvars then []
@@ -212,7 +212,7 @@
   fun map_check_aux rty warns =
     case rty of
       Type (_, []) => warns
-    | Type (s, _) => if (maps_defined thy s) then warns else s::warns
+    | Type (s, _) => if maps_defined thy s then warns else s::warns
     | _ => warns
 
   val warns = map_check_aux rty []
@@ -255,7 +255,7 @@
   val goals = map (mk_goal o snd) quot_list
               
   fun after_qed thms lthy =
-    fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
+    fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd
 in
   theorem after_qed goals lthy
 end