diff -r c95afd0dc594 -r 5e74bd87bcda Nominal/Ex/SFT/Theorem.thy
--- a/Nominal/Ex/SFT/Theorem.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/Theorem.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -55,7 +55,7 @@
   fixes F :: lam
   shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>"
 proof -
-  obtain x :: var where [simp]:"atom x \<sharp> F" using obtain_fresh by blast
+  obtain x :: name where [simp]:"atom x \<sharp> F" using obtain_fresh by blast
   def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))"
   def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>"
   have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def ..