src/HOL/Unix/Nested_Environment.thy

   nested environment).  A \emph{defined position} within a nested
   environment is one where @{term lookup} at its path does not yield
   @{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
         [] => Some (Env b es)
       | y # ys => lookup_option (es y) ys)"

   delete an existing entry, or overwrite an existing one.  Note that
   update at undefined positions is simple absorbed, i.e.\ the
   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
 
 text {*
   \medskip The characteristic cases of @{term update} are expressed by