diff -r 89a2ff3f82c7 -r df05cd030d2f FSet.thy
--- a/FSet.thy	Wed Oct 28 10:29:00 2009 +0100
+++ b/FSet.thy	Wed Oct 28 15:25:11 2009 +0100
@@ -36,7 +36,7 @@
 
 ML {* @{term "Abs_fset"} *}
 local_setup {*
-  make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term Nil
@@ -45,7 +45,7 @@
 
 
 local_setup {*
-  make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term Cons
@@ -53,7 +53,7 @@
 thm INSERT_def
 
 local_setup {*
-  make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term append
@@ -78,7 +78,7 @@
 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
 local_setup {*
-  make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term card1
@@ -143,7 +143,7 @@
   done
 
 local_setup {*
-  make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term membship
@@ -151,7 +151,7 @@
 thm IN_def
 
 local_setup {*
-  make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term fold1
@@ -159,7 +159,7 @@
 thm fold_def
 
 local_setup {*
-  make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn 
+  old_make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn 
   @{typ "'a list"} @{typ "'a fset"} #> snd
 *}