--- a/src/HOL/Tools/primrec_package.ML Mon Aug 29 16:18:03 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML Mon Aug 29 16:18:04 2005 +0200
@@ -72,11 +72,11 @@
(check_vars "repeated variable names in pattern: " (duplicates lfrees);
check_vars "extra variables on rhs: "
(map dest_Free (term_frees rhs) \\ lfrees);
- case assoc (rec_fns, fnameT) of
+ case AList.lookup (op =) rec_fns fnameT of
NONE =>
(fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
| SOME (_, rpos', eqns) =>
- if isSome (assoc (eqns, cname)) then
+ if AList.defined (op =) eqns cname then
raise RecError "constructor already occurred as pattern"
else if rpos <> rpos' then
raise RecError "position of recursive argument inconsistent"
@@ -104,7 +104,7 @@
if is_Const f andalso dest_Const f mem map fst rec_eqns then
let
val fnameT' as (fname', _) = dest_Const f;
- val (_, rpos, _) = valOf (assoc (rec_eqns, fnameT'));
+ val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
val ls = Library.take (rpos, ts);
val rest = Library.drop (rpos, ts);
val (x', rs) = (hd rest, tl rest)
@@ -112,7 +112,7 @@
\ in recursive application\nof function " ^ quote fname' ^ " on rhs");
val (x, xs) = strip_comb x'
in
- (case assoc (subs, x) of
+ (case AList.lookup (op =) subs x of
NONE =>
let
val (fs', ts') = foldl_map (subst subs) (fs, ts)
@@ -134,7 +134,7 @@
(* translate rec equations into function arguments suitable for rec comb *)
fun trans eqns ((cname, cargs), (fnameTs', fnss', fns)) =
- (case assoc (eqns, cname) of
+ (case AList.lookup (op =) eqns cname of
NONE => (warning ("No equation for constructor " ^ quote cname ^
"\nin definition of function " ^ quote fname);
(fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
@@ -154,13 +154,13 @@
(list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)
end)
- in (case assoc (fnameTs, i) of
+ in (case AList.lookup (op =) fnameTs i of
NONE =>
if exists (equal fnameT o snd) fnameTs then
raise RecError ("inconsistent functions for datatype " ^ quote tname)
else
let
- val (_, _, eqns) = valOf (assoc (rec_eqns, fnameT));
+ val (_, _, eqns) = the (AList.lookup (op =) rec_eqns fnameT);
val (fnameTs', fnss', fns) = foldr (trans eqns)
((i, fnameT)::fnameTs, fnss, []) constrs
in
@@ -175,7 +175,7 @@
(* prepare functions needed for definitions *)
fun get_fns fns (((i, (tname, _, constrs)), rec_name), (fs, defs)) =
- case assoc (fns, i) of
+ case AList.lookup (op =) fns i of
NONE =>
let
val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
@@ -216,7 +216,7 @@
let
fun constrs_of (_, (_, _, cs)) =
map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
- val params_of = Library.assocs (List.concat (map constrs_of rec_eqns));
+ val params_of = these o AList.lookup (op =) (List.concat (map constrs_of rec_eqns));
in
induction
|> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr)))