--- a/quotient.ML	Mon Oct 12 23:06:14 2009 +0200
+++ b/quotient.ML	Mon Oct 12 23:16:20 2009 +0200
@@ -94,7 +94,7 @@
 end
 
 (* main function for constructing the quotient type *)
-fun typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy =
+fun mk_typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy =
 let
   (* generates typedef *)
   val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
@@ -169,18 +169,12 @@
 
   val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm)
-		   
-  val _ = [Syntax.string_of_term lthy EQUIV_goal,
-           Syntax.string_of_typ lthy (fastype_of rel_trm),
-           Syntax.string_of_typ lthy EQUIV_ty]
-          |> cat_lines
-          |> tracing
- 
+		    
   fun after_qed thms lthy =
   let
     val thm = the_single (flat thms)
   in
-    typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd   
+    mk_typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd   
   end
 in
   Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy