--- a/QuotMain.thy	Tue Aug 11 12:29:15 2009 +0200
+++ b/QuotMain.thy	Tue Aug 18 14:04:51 2009 +0200
@@ -71,24 +71,19 @@
 
 end
 
-ML {*
-  Variable.variant_frees
-*}
-
-
 section {* type definition for the quotient type *}
 
 ML {*
-(* constructs the term \<lambda>(c::ty\<Rightarrow>bool). \<exists>x. c = rel x *)
+(* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)
 fun typedef_term rel ty lthy =
 let 
   val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] 
                |> Variable.variant_frees lthy [rel]
                |> map Free
 in
-  lambda c  
-    ((HOLogic.exists_const ty) $ 
-      (lambda x (HOLogic.mk_eq (c, (rel $ x)))))
+  lambda c 
+    (HOLogic.mk_exists 
+       ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
 end
 *}
 
@@ -102,7 +97,7 @@
 (* makes the new type definitions *)
 fun typedef_make (qty_name, rel, ty) lthy =
   LocalTheory.theory_result
-  (TypedefPackage.add_typedef false NONE 
+  (Typedef.add_typedef false NONE 
      (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
        (typedef_term rel ty lthy)
          NONE typedef_tac) lthy
@@ -110,7 +105,7 @@
 
 text {* proves the QUOTIENT theorem for the new type *}
 ML {*
-fun typedef_quot_type_tac equiv_thm (typedef_info: TypedefPackage.info) = 
+fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = 
 let
   val rep_thm = #Rep typedef_info
   val rep_inv = #Rep_inverse typedef_info