diff -r 426834f253c8 -r 04f64e602fa6 src/HOL/Unix/Nested_Environment.thy
--- a/src/HOL/Unix/Nested_Environment.thy	Tue Aug 30 17:02:06 2011 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy	Tue Aug 30 17:36:12 2011 +0200
@@ -43,9 +43,9 @@
   @{term None}.
 *}
 
-primrec
-  lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
-  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
+primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
+  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
+where
     "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
   | "lookup (Env b es) xs =
       (case xs of
@@ -245,22 +245,22 @@
   environment is left unchanged.
 *}
 
-primrec
-  update :: "'c list => ('a, 'b, 'c) env option
-    => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
-  and update_option :: "'c list => ('a, 'b, 'c) env option
-    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
-    "update xs opt (Val a) =
-      (if xs = [] then (case opt of None => Val a | Some e => e)
-      else Val a)"
-  | "update xs opt (Env b es) =
-      (case xs of
-        [] => (case opt of None => Env b es | Some e => e)
-      | y # ys => Env b (es (y := update_option ys opt (es y))))"
-  | "update_option xs opt None =
-      (if xs = [] then opt else None)"
-  | "update_option xs opt (Some e) =
-      (if xs = [] then opt else Some (update xs opt e))"
+primrec update :: "'c list => ('a, 'b, 'c) env option =>
+    ('a, 'b, 'c) env => ('a, 'b, 'c) env"
+  and update_option :: "'c list => ('a, 'b, 'c) env option =>
+    ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
+where
+  "update xs opt (Val a) =
+    (if xs = [] then (case opt of None => Val a | Some e => e)
+     else Val a)"
+| "update xs opt (Env b es) =
+    (case xs of
+      [] => (case opt of None => Env b es | Some e => e)
+    | y # ys => Env b (es (y := update_option ys opt (es y))))"
+| "update_option xs opt None =
+    (if xs = [] then opt else None)"
+| "update_option xs opt (Some e) =
+    (if xs = [] then opt else Some (update xs opt e))"
 
 hide_const update_option