--- a/Nominal/Ex/SFT/Utils.thy	Wed Dec 21 14:25:05 2011 +0900
+++ b/Nominal/Ex/SFT/Utils.thy	Wed Dec 21 15:43:58 2011 +0900
@@ -1,9 +1,9 @@
 header {* Utilities for defining constants and functions *}
 
-theory Utils imports Lambda begin
+theory Utils imports LambdaTerms begin
 
 lemma beta_app:
-  "(\<integral> x. M) \<cdot> V x \<approx> M"
+  "(\<integral> x. M) \<cdot> Var x \<approx> M"
   by (rule b3, rule bI)
      (simp add: b1)
 
@@ -72,7 +72,7 @@
     done
   qed
 
-definition cn :: "nat \<Rightarrow> var" where "cn n \<equiv> Abs_var (Atom (Sort ''Lambda.var'' []) n)"
+definition cn :: "nat \<Rightarrow> var" where "cn n \<equiv> Abs_var (Atom (Sort ''LambdaTerms.var'' []) n)"
 
 lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n"
   unfolding cn_def using Abs_var_inject by simp