--- a/Quot/quotient_typ.ML	Wed Feb 10 17:10:52 2010 +0100
+++ b/Quot/quotient_typ.ML	Wed Feb 10 17:22:18 2010 +0100
@@ -79,7 +79,7 @@
 end
 
 
-(* tactic to prove the Quot_Type theorem for the new type *)
+(* 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
@@ -87,7 +87,7 @@
   val abs_inv = mem_def2 RS #Abs_inverse typedef_info
   val rep_inj = #Rep_inject typedef_info
 in
-  (rtac @{thm Quot_Type.intro} THEN' RANGE [
+  (rtac @{thm quot_type.intro} THEN' RANGE [
     rtac equiv_thm,
     rtac rep_thm,
     rtac rep_inv,
@@ -96,10 +96,10 @@
 end
 
 
-(* proves the Quot_Type theorem for the new type *)
+(* 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)
+  val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
   val goal =
     HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
     |> Syntax.check_term lthy
@@ -119,7 +119,7 @@
   val typedef_quotient_thm_tac =
     EVERY1 [
       K (rewrite_goals_tac [abs_def, rep_def]),
-      rtac @{thm Quot_Type.Quotient},
+      rtac @{thm quot_type.Quotient},
       rtac quot_type_thm]
 in
   Goal.prove lthy [] [] goal
@@ -142,8 +142,8 @@
   val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
 
   (* more useful 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_const)
   val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
   val abs_name = Binding.prefix_name "abs_" qty_name