src/HOL/Library/Nested_Environment.thy

 
 theorem lookup_append_none:
   assumes "lookup env xs = None"
   shows "lookup env (xs @ ys) = None"
   using prems
-proof (induct xs fixing: env)
+proof (induct xs arbitrary: env)
   case Nil
   then have False by simp
   then show ?case ..
 next
   case (Cons x xs)

 
 theorem lookup_append_some:
   assumes "lookup env xs = Some e"
   shows "lookup env (xs @ ys) = lookup e ys"
   using prems
-proof (induct xs fixing: env e)
+proof (induct xs arbitrary: env e)
   case Nil
   then have "env = e" by simp
   then show "lookup env ([] @ ys) = lookup e ys" by simp
 next
   case (Cons x xs)

   shows "\<exists>b' es' env'.
     lookup env xs = Some (Env b' es') \<and>
     es' y = Some env' \<and>
     lookup env' ys = Some e"
   using prems
-proof (induct xs fixing: env e)
+proof (induct xs arbitrary: env e)
   case Nil
   from Nil.prems have "lookup env (y # ys) = Some e"
     by simp
   then obtain b' es' env' where
       env: "env = Env b' es'" and

 
 theorem lookup_update_some:
   assumes "lookup env xs = Some e"
   shows "lookup (update xs (Some env') env) xs = Some env'"
   using prems
-proof (induct xs fixing: env e)
+proof (induct xs arbitrary: env e)
   case Nil
   then have "env = e" by simp
   then show ?case by simp
 next
   case (Cons x xs)

 
 theorem update_append_none:
   assumes "lookup env xs = None"
   shows "update (xs @ y # ys) opt env = env"
   using prems
-proof (induct xs fixing: env)
+proof (induct xs arbitrary: env)
   case Nil
   then have False by simp
   then show ?case ..
 next
   case (Cons x xs)

 
 theorem update_append_some:
   assumes "lookup env xs = Some e"
   shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
   using prems
-proof (induct xs fixing: env e)
+proof (induct xs arbitrary: env e)
   case Nil
   then have "env = e" by simp
   then show ?case by simp
 next
   case (Cons x xs)

 
 theorem lookup_update_other:
   assumes neq: "y \<noteq> (z::'c)"
   shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
     lookup env (xs @ y # ys)"
-proof (induct xs fixing: env)
+proof (induct xs arbitrary: env)
   case Nil
   show ?case
   proof (cases env)
     case Val
     then show ?thesis by simp