--- 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