src/HOL/Library/Nested_Environment.thy

--- a/src/HOL/Library/Nested_Environment.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -216,7 +216,7 @@
       es' y = Some env' \<and>
       lookup env' ys = Some e"
   (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs")
-proof (induct ?P xs)
+proof (induct xs)
   fix env e let ?A = "?A env e" and ?C = "?C env e"
   {
     assume "?A []"