--- a/IntEx.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 15:48:38 2009 +0100
@@ -45,9 +45,10 @@
 where
   "my_neg (x, y) = (y, x)"
 
-local_setup {*
-  old_make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
+quotient_def (for my_int)
+  NEG::"my_int \<Rightarrow> my_int"
+where
+  "NEG \<equiv> my_neg"
 
 term NEG
 thm NEG_def
@@ -62,9 +63,10 @@
 where
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-local_setup {*
-  old_make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
+quotient_def (for my_int)
+  MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+where
+  "MULT \<equiv> my_mult"
 
 term MULT
 thm MULT_def
@@ -75,9 +77,10 @@
 where
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
-local_setup {*
-  old_make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
+quotient_def (for my_int)
+  LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
+where
+  "LE \<equiv> my_le"
 
 term LE
 thm LE_def
@@ -90,7 +93,6 @@
 term LESS
 thm LESS_def
 
-
 definition
   ABS :: "my_int \<Rightarrow> my_int"
 where
@@ -148,12 +150,6 @@
  ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
 
 
-
-
-
-
-
-
 text {* Below is the construction site code used if things do now work *}
 
 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *}