--- a/QuotMain.thy	Mon Oct 05 11:24:32 2009 +0200
+++ b/QuotMain.thy	Mon Oct 05 11:54:02 2009 +0200
@@ -154,25 +154,28 @@
     (HOLogic.exists_const ty $
        lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
-
+*}
 
+ML {*
 (* makes the new type definitions and proves non-emptyness*)
-fun typedef_make (qty_name, rel, ty) lthy =
+fun typedef_make (qty_name, mx, rel, ty) lthy =
 let
   val typedef_tac =
      EVERY1 [rewrite_goal_tac @{thms mem_def},
              rtac @{thm exI},
              rtac @{thm exI},
              rtac @{thm refl}]
+  val tfrees = map fst (Term.add_tfreesT ty [])
 in
   LocalTheory.theory_result
     (Typedef.add_typedef false NONE
-       (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
+       (qty_name, tfrees, mx)
          (typedef_term rel ty lthy)
            NONE typedef_tac) lthy
 end
+*}
 
-
+ML {*
 (* tactic to prove the QUOT_TYPE theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
@@ -251,10 +254,10 @@
 *}
 
 ML {*
-fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
+fun typedef_main (qty_name, mx, rel, ty, equiv_thm) lthy =
 let
   (* generates typedef *)
-  val ((_, typedef_info), lthy1) = typedef_make (qty_name, rel, ty) lthy
+  val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, ty) lthy
 
   (* abs and rep functions *)
   val abs_ty = #abs_type typedef_info
@@ -331,7 +334,7 @@
   r_eq: "EQUIV RR"
 
 local_setup {*
-  typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
+  typedef_main (@{binding "qtrm"}, NoSyn, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
 *}
 
 term Rep_qtrm
@@ -360,7 +363,7 @@
 
 
 local_setup {*
-  typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
+  typedef_main (@{binding "qtrm'"}, NoSyn, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
 *}
 
 print_theorems
@@ -382,7 +385,7 @@
 axioms t_eq: "EQUIV Rt"
 
 local_setup {*
-  typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
+  typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
 *}
 
 section {* lifting of constants *}
@@ -534,7 +537,7 @@
 
 
 local_setup {*
-  typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
+  typedef_main (@{binding "qt'"}, NoSyn, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
 *}
 
 print_theorems
@@ -579,7 +582,7 @@
   done
 
 local_setup {*
-  typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
+  typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
 *}
 
 print_theorems