diff -r 421f8bc19ce4 -r 2814ff2a6e3e src/HOL/Bali/DefiniteAssignment.thy --- a/src/HOL/Bali/DefiniteAssignment.thy Sun Jul 31 11:13:38 2011 -0700 +++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Aug 01 12:08:53 2011 +0200 @@ -1056,8 +1056,7 @@ (is "PROP ?Hyp Env B t A") proof (induct) case Skip - from Skip.prems Skip.hyps - show ?case by cases simp + then show ?case by cases simp next case Expr from Expr.prems Expr.hyps