1.1 --- a/src/HOL/Unix/Nested_Environment.thy	Tue Aug 30 17:02:06 2011 +0200
     1.2 +++ b/src/HOL/Unix/Nested_Environment.thy	Tue Aug 30 17:36:12 2011 +0200
     1.3 @@ -43,9 +43,9 @@
     1.4    @{term None}.
     1.5  *}
     1.6  
     1.7 -primrec
     1.8 -  lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
     1.9 -  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
    1.10 +primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
    1.11 +  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
    1.12 +where
    1.13      "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
    1.14    | "lookup (Env b es) xs =
    1.15        (case xs of
    1.16 @@ -245,22 +245,22 @@
    1.17    environment is left unchanged.
    1.18  *}
    1.19  
    1.20 -primrec
    1.21 -  update :: "'c list => ('a, 'b, 'c) env option
    1.22 -    => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
    1.23 -  and update_option :: "'c list => ('a, 'b, 'c) env option
    1.24 -    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
    1.25 -    "update xs opt (Val a) =
    1.26 -      (if xs = [] then (case opt of None => Val a | Some e => e)
    1.27 -      else Val a)"
    1.28 -  | "update xs opt (Env b es) =
    1.29 -      (case xs of
    1.30 -        [] => (case opt of None => Env b es | Some e => e)
    1.31 -      | y # ys => Env b (es (y := update_option ys opt (es y))))"
    1.32 -  | "update_option xs opt None =
    1.33 -      (if xs = [] then opt else None)"
    1.34 -  | "update_option xs opt (Some e) =
    1.35 -      (if xs = [] then opt else Some (update xs opt e))"
    1.36 +primrec update :: "'c list => ('a, 'b, 'c) env option =>
    1.37 +    ('a, 'b, 'c) env => ('a, 'b, 'c) env"
    1.38 +  and update_option :: "'c list => ('a, 'b, 'c) env option =>
    1.39 +    ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
    1.40 +where
    1.41 +  "update xs opt (Val a) =
    1.42 +    (if xs = [] then (case opt of None => Val a | Some e => e)
    1.43 +     else Val a)"
    1.44 +| "update xs opt (Env b es) =
    1.45 +    (case xs of
    1.46 +      [] => (case opt of None => Env b es | Some e => e)
    1.47 +    | y # ys => Env b (es (y := update_option ys opt (es y))))"
    1.48 +| "update_option xs opt None =
    1.49 +    (if xs = [] then opt else None)"
    1.50 +| "update_option xs opt (Some e) =
    1.51 +    (if xs = [] then opt else Some (update xs opt e))"
    1.52  
    1.53  hide_const update_option
    1.54