diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Simple/Common.thy --- a/src/HOL/UNITY/Simple/Common.thy Wed May 25 11:49:40 2016 +0200 +++ b/src/HOL/UNITY/Simple/Common.thy Wed May 25 11:50:58 2016 +0200 @@ -97,7 +97,7 @@ then show ?case by simp qed next - from `n \ common` + from \n \ common\ show "{..n} \ id -` {n..} \ common \ common" by (simp add: atMost_Int_atLeast) qed