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