--- a/QuotMain.thy	Mon Oct 12 23:06:14 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 23:16:20 2009 +0200
@@ -142,25 +142,11 @@
 end
 
 section {* type definition for the quotient type *}
-ML {* Binding.name *}
-
-ML {* cat_lines *}
 
 use "quotient.ML"
 
-ML {*
-  mk_typedef;
-  mk_typedef_cmd;
-  quottype_parser
-*}
-
-ML {* Proof.theorem_i *}
-
 term EQUIV
 
-ML {* quottype_parser *}
-ML {* OuterSyntax.local_theory_to_proof *}
-
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
   let
@@ -184,12 +170,6 @@
   apply(rule r_eq)
   done
 
-(*
-local_setup {*
-  typedef_main (@{binding "qtrm"}, NoSyn, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
-*}
-*)
-
 typ qtrm
 term Rep_qtrm
 term REP_qtrm
@@ -216,12 +196,6 @@
 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 
-(*
-local_setup {*
-  typedef_main (@{binding "qtrm'"}, NoSyn, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
-*}
-*)
-
 quotient "'a qtrm'" = "'a trm'" / "R'"
   apply(rule r_eq')
   done
@@ -244,12 +218,6 @@
 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
 axioms t_eq: "EQUIV Rt"
 
-(*
-local_setup {*
-  typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
-*}
-*)
-
 quotient "qt" = "t" / "Rt"
   by (rule t_eq)
 
@@ -440,12 +408,6 @@
 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 axioms t_eq': "EQUIV Rt'"
 
-(*
-local_setup {*
-  typedef_main (@{binding "qt'"}, NoSyn, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
-*}
-*)
-
 quotient "'a qt'" = "'a t'" / "Rt'"
   apply(rule t_eq')
   done
@@ -491,12 +453,6 @@
   apply(auto intro: list_eq.intros list_eq_refl)
   done
 
-(*
-local_setup {*
-  typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
-*}
-*)
-
 quotient "'a fset" = "'a list" / "list_eq"
   apply(rule equiv_list_eq)
   done

--- 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