# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1253891330 -7200
# Node ID 980d45c4a72647d12d0f2a229d3137cf56f51773
# Parent  cac00e8b972b9149cd45b963202c7a36f759c3dc
fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x

diff -r cac00e8b972b -r 980d45c4a726 QuotMain.thy
--- 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 =