--- a/Quot/quotient_term.ML	Tue Feb 09 14:32:37 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Feb 09 15:28:15 2010 +0100
@@ -9,7 +9,7 @@
 sig
   exception LIFT_MATCH of string
 
-  datatype flag = absF | repF
+  datatype flag = AbsF | RepF
 
   val absrep_fun: flag -> Proof.context -> typ * typ -> term
   val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
@@ -41,15 +41,15 @@
 (*** Aggregate Rep/Abs Function ***)
 
 
-(* The flag repF is for types in negative position; absF is for types 
+(* The flag RepF is for types in negative position; AbsF is for types 
    in positive position. Because of this, function types need to be   
    treated specially, since there the polarity changes.               
 *)
 
-datatype flag = absF | repF
+datatype flag = AbsF | RepF
 
-fun negF absF = repF
-  | negF repF = absF
+fun negF AbsF = RepF
+  | negF RepF = AbsF
 
 fun is_identity (Const (@{const_name "id"}, _)) = true
   | is_identity _ = false
@@ -58,8 +58,8 @@
 
 fun mk_fun_compose flag (trm1, trm2) = 
   case flag of
-    absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
-  | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
+    AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
+  | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
 
 fun get_mapfun ctxt s =
 let
@@ -134,8 +134,8 @@
   val qty_name = Long_Name.base_name qty_str
 in
   case flag of
-    absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
-  | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
+    AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
+  | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
@@ -620,7 +620,7 @@
 *)
 
 fun mk_repabs ctxt (T, T') trm = 
-  absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm)
+  absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
 
 fun inj_repabs_err ctxt msg rtrm qtrm =
 let