diff -r 8f51702e1f2e -r 52730e5ec8cb Nominal/Ex/SFT/Consts.thy
--- a/Nominal/Ex/SFT/Consts.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/Ex/SFT/Consts.thy	Thu May 24 10:17:32 2012 +0200
@@ -285,10 +285,10 @@
   apply (rule lam2_fast_app, rule Lam_A, simp_all)
   done
 
-definition "Num \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>"
+definition "NUM \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>"
 
-lemma supp_Num[simp]:
-  "supp Num = {}"
-  by (auto simp only: Num_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil)
+lemma supp_NUM[simp]:
+  "supp NUM = {}"
+  by (auto simp only: NUM_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil)
 
 end