diff -r 45a79edbe73b -r 1941b3315952 src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Fri Mar 11 08:12:58 2011 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Mar 11 08:12:59 2011 +0100
@@ -302,15 +302,15 @@
 fun mk_fun_upd T1 T2 (t1, t2) t = 
   Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
 
-fun dest_plain_fun t =
+fun dest_fun_upds t =
   case try dest_fun_upd t of
     NONE =>
       (case t of
         Abs (_, _, _) => ([], t) 
-      | _ => raise TERM ("dest_plain_fun", [t]))
-  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_plain_fun t0)
+      | _ => raise TERM ("dest_fun_upds", [t]))
+  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
 
-fun make_plain_fun T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
+fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
 
 fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
@@ -344,7 +344,7 @@
   in
     case fastype_of t of
       Type (@{type_name fun}, [T1, T2]) =>
-        (case try dest_plain_fun t of
+        (case try dest_fun_upds t of
           SOME (tps, t) =>
             (map (pairself post_process_term) tps, map_Abs post_process_term t)
             |> (case T2 of
@@ -352,12 +352,14 @@
                 (case t of
                    Abs(_, _, @{const True}) => fst #> rev #> make_set T1
                  | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
+                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
                  | _ => raise TERM ("post_process_term", [t]))
             | Type (@{type_name option}, _) =>
                 (case t of
-                  Abs(_, _, Const(@{const_name None}, _)) => fst #> (make_map T1 T2)
-                | _ => make_plain_fun T1 T2) 
-            | _ => make_plain_fun T1 T2)
+                  Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
+                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
+                | _ => make_fun_upds T1 T2) 
+            | _ => make_fun_upds T1 T2)
         | NONE => raise TERM ("post_process_term", [t]))
     | _ => process_args t
   end