# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258842181 -3600
# Node ID 5d06e1dba69aa8be55d9401d09f190e2a7ef798c
# Parent  491dde407f405fea7610090f540d8d83bd8165e4
slight tuning

diff -r 491dde407f40 -r 5d06e1dba69a IntEx.thy
--- a/IntEx.thy	Sat Nov 21 14:45:25 2009 +0100
+++ b/IntEx.thy	Sat Nov 21 23:23:01 2009 +0100
@@ -119,6 +119,8 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
+
+
 ML {* print_qconstinfo @{context} *}
 
 ML {* print_qconstinfo @{context} *}
diff -r 491dde407f40 -r 5d06e1dba69a quotient.ML
--- a/quotient.ML	Sat Nov 21 14:45:25 2009 +0100
+++ b/quotient.ML	Sat Nov 21 23:23:01 2009 +0100
@@ -39,8 +39,8 @@
 end
 
 
-(* definition of the quotient type *)
-(***********************************)
+(* definition of quotient types *)
+(********************************)
 
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =
diff -r 491dde407f40 -r 5d06e1dba69a quotient_def.ML
--- a/quotient_def.ML	Sat Nov 21 14:45:25 2009 +0100
+++ b/quotient_def.ML	Sat Nov 21 23:23:01 2009 +0100
@@ -24,11 +24,6 @@
   ((rhs, thm), lthy')
 end
 
-(* calculates the aggregate abs and rep functions for a given type; 
-   repF is for constants' arguments; absF is for constants;
-   function types need to be treated specially, since repF and absF
-   change *)
-
 datatype flag = absF | repF
 
 fun negF absF = repF
@@ -72,6 +67,12 @@
   | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
 end
 
+
+(* calculates the aggregate abs and rep functions for a given type; 
+   repF is for constants' arguments; absF is for constants;
+   function types need to be treated specially, since repF and absF
+   change *)
+
 fun get_fun flag lthy (rty, qty) =
   case (rty, qty) of 
     (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
@@ -96,7 +97,7 @@
   | (TVar _, TVar _) => ty_lift_error2 lthy rty qty
   | _ => ty_lift_error1 lthy rty qty
 
-fun make_def nconst_bname qty mx attr rhs lthy =
+fun make_def qconst_bname qty mx attr rhs lthy =
 let
   val rty = fastype_of rhs
   val (arg_rtys, res_rty) = strip_type rty
@@ -111,12 +112,12 @@
   val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)
                    |> Syntax.check_term lthy 
 
-  val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy
+  val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
 
-  val nconst_str = Binding.name_of nconst_bname
+  val qconst_str = Binding.name_of qconst_bname
   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs}
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen nconst_str (qcinfo phi)) lthy'
+                 (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end
diff -r 491dde407f40 -r 5d06e1dba69a quotient_info.ML
--- a/quotient_info.ML	Sat Nov 21 14:45:25 2009 +0100
+++ b/quotient_info.ML	Sat Nov 21 23:23:01 2009 +0100
@@ -45,7 +45,6 @@
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
-(* FIXME: this should be done using a generic context *)
 
 fun maps_attribute_aux s minfo = Thm.declaration_attribute 
   (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
@@ -72,7 +71,7 @@
            "declaration of map information"))
 
 
-(* info about the quotient types *)
+(* info about quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
 structure QuotData = Theory_Data
@@ -117,7 +116,7 @@
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
 
-(* environments of quotient and raw types *)
+(* FIXME: obsolete: environments for quotient and raw types *)
 type qenv = (typ * typ) list
 
 fun mk_qenv ctxt =