--- a/QuotMain.thy	Fri Sep 25 16:50:11 2009 +0200
+++ b/QuotMain.thy	Fri Sep 25 17:08:50 2009 +0200
@@ -151,11 +151,19 @@
                |> map Free
 in
   lambda c
-    (HOLogic.mk_exists
-       ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
+    (HOLogic.exists_const ty $ 
+       lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
 *}
 
+
+ML {*
+  typedef_term @{term "x::nat\<Rightarrow>nat\<Rightarrow>bool"} @{typ nat} @{context}
+  |> Syntax.string_of_term @{context} 
+  |> writeln
+*}
+
+
 ML {*
 (* makes the new type definitions and proves non-emptyness*)
 fun typedef_make (qty_name, rel, ty) lthy =