src/HOL/IMP/Big_Step.thy

--- a/src/HOL/IMP/Big_Step.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -37,7 +37,7 @@
 text{* For inductive definitions we need command
        \texttt{values} instead of \texttt{value}. *}
 
-values "{t. (SKIP, %_. 0) \<Rightarrow> t}"
+values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}"
 
 text{* We need to translate the result state into a list
 to display it. *}