--- a/Quot/Examples/FSet3.thy	Fri Dec 11 17:03:52 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Dec 11 17:22:26 2009 +0100
@@ -22,7 +22,8 @@
 quotient fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
-lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry
+lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A"
+unfolding list_eq_def by auto
 
 (* The 2 lemmas below are different from the ones in QuotList *)
 lemma nil_rsp[quot_respect]:

--- a/Quot/Examples/IntEx2.thy	Fri Dec 11 17:03:52 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Dec 11 17:22:26 2009 +0100
@@ -194,8 +194,8 @@
    (simp)
 
 lemma add:
-     "(ABS_int (x,y)) + (ABS_int (u,v)) =
-      (ABS_int (x + u, y + v))"
+     "(abs_int (x,y)) + (abs_int (u,v)) =
+      (abs_int (x + u, y + v))"
 apply(simp add: plus_int_def)
 apply(fold plus_raw.simps)
 apply(rule Quotient_rel_abs[OF Quotient_int])

--- a/Quot/QuotMain.thy	Fri Dec 11 17:03:52 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 17:22:26 2009 +0100
@@ -17,14 +17,14 @@
 begin
 
 definition
-  ABS::"'a \<Rightarrow> 'b"
+  abs::"'a \<Rightarrow> 'b"
 where
-  "ABS x \<equiv> Abs (R x)"
+  "abs x \<equiv> Abs (R x)"
 
 definition
-  REP::"'b \<Rightarrow> 'a"
+  rep::"'b \<Rightarrow> 'a"
 where
-  "REP a = Eps (Rep a)"
+  "rep a = Eps (Rep a)"
 
 lemma lem9:
   shows "R (Eps (R x)) = R x"
@@ -36,9 +36,9 @@
 qed
 
 theorem thm10:
-  shows "ABS (REP a) \<equiv> a"
+  shows "abs (rep a) \<equiv> a"
   apply  (rule eq_reflection)
-  unfolding ABS_def REP_def
+  unfolding abs_def rep_def
 proof -
   from rep_prop
   obtain x where eq: "Rep a = R x" by auto
@@ -50,9 +50,9 @@
   show "Abs (R (Eps (Rep a))) = a" by simp
 qed
 
-lemma REP_refl:
-  shows "R (REP a) (REP a)"
-unfolding REP_def
+lemma rep_refl:
+  shows "R (rep a) (rep a)"
+unfolding rep_def
 by (simp add: equivp[simplified equivp_def])
 
 lemma lem7:
@@ -64,21 +64,21 @@
 done
 
 theorem thm11:
-  shows "R r r' = (ABS r = ABS r')"
-unfolding ABS_def
+  shows "R r r' = (abs r = abs r')"
+unfolding abs_def
 by (simp only: equivp[simplified equivp_def] lem7)
 
 
-lemma REP_ABS_rsp:
-  shows "R f (REP (ABS g)) = R f g"
-  and   "R (REP (ABS g)) f = R g f"
+lemma rep_abs_rsp:
+  shows "R f (rep (abs g)) = R f g"
+  and   "R (rep (abs g)) f = R g f"
 by (simp_all add: thm10 thm11)
 
 lemma Quotient:
-  "Quotient R ABS REP"
+  "Quotient R abs rep"
 apply(unfold Quotient_def)
 apply(simp add: thm10)
-apply(simp add: REP_refl)
+apply(simp add: rep_refl)
 apply(subst thm11[symmetric])
 apply(simp add: equivp[simplified equivp_def])
 done

--- a/Quot/ROOT.ML	Fri Dec 11 17:03:52 2009 +0100
+++ b/Quot/ROOT.ML	Fri Dec 11 17:22:26 2009 +0100
@@ -4,8 +4,10 @@
    ["QuotMain",
     "Examples/FSet",
     "Examples/FSet2",
+    "Examples/FSet3",
     "Examples/IntEx",
     "Examples/IntEx2",
     "Examples/LFex",
     "Examples/LamEx",
-    "Examples/LarryDatatype"];
+    "Examples/LarryDatatype",
+    "Examples/LarryInt"];

--- a/Quot/quotient.ML	Fri Dec 11 17:03:52 2009 +0100
+++ b/Quot/quotient.ML	Fri Dec 11 17:22:26 2009 +0100
@@ -132,12 +132,12 @@
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
   (* ABS and REP definitions *)
-  val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
-  val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
+  val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT )
+  val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT )
   val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
   val REP_trm = Syntax.check_term lthy1 (REP_const $ rep)
-  val ABS_name = Binding.prefix_name "ABS_" qty_name
-  val REP_name = Binding.prefix_name "REP_" qty_name
+  val ABS_name = Binding.prefix_name "abs_" qty_name
+  val REP_name = Binding.prefix_name "rep_" qty_name
   val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
          lthy1 |> define (ABS_name, NoSyn, ABS_trm)
                ||>> define (REP_name, NoSyn, REP_trm)

--- a/Quot/quotient_def.ML	Fri Dec 11 17:03:52 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Dec 11 17:22:26 2009 +0100
@@ -31,18 +31,18 @@
 fun get_fun_aux lthy s fs =
   case (maps_lookup (ProofContext.theory_of lthy) s) of
     SOME info => list_comb (Const (#mapfun info, dummyT), fs)
-  | NONE      => raise 
+  | NONE      => raise
         (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
 
 fun get_const flag lthy _ qty =
 (* FIXME: check here that _ and qty are related *)
-let 
+let
   val thy = ProofContext.theory_of lthy
   val qty_name = Long_Name.base_name (fst (dest_Type qty))
 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
 
 
@@ -53,17 +53,17 @@
 
 fun get_fun flag lthy (rty, qty) =
   if rty = qty then mk_identity qty else
-  case (rty, qty) of 
+  case (rty, qty) of
     (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
      let
        val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
        val fs_ty2 = get_fun flag lthy (ty2, ty2')
-     in  
+     in
        get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
-     end 
+     end
   | (Type (s, []), Type (s', [])) =>
      if s = s'
-     then mk_identity qty 
+     then mk_identity qty
      else get_const flag lthy rty qty
   | (Type (s, tys), Type (s', tys')) =>
      if s = s'
@@ -71,7 +71,7 @@
      else get_const flag lthy rty qty
   | (TFree x, TFree x') =>
      if x = x'
-     then mk_identity qty 
+     then mk_identity qty
      else raise (LIFT_MATCH "get_fun")
   | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
   | _ => raise (LIFT_MATCH "get_fun")