alist_rec and assoc are now defined using primrec and thus no longer
refer to the recursion combinator list_rec, which should be considered
internal.

--- a/src/HOL/Subst/AList.ML	Mon May 15 17:30:19 2000 +0200
+++ b/src/HOL/Subst/AList.ML	Mon May 15 17:32:39 2000 +0200
@@ -8,20 +8,6 @@
 
 open AList;
 
-let fun prove s = prove_goalw AList.thy [alist_rec_def,assoc_def] s 
-			  (fn _ => [Simp_tac 1])
-in 
-Addsimps 
- (
-   map prove 
-   ["alist_rec [] c d = c",
-    "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)",
-    "assoc v d [] = d",
-    "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] 
- )
-end;
-
-
 val prems = goal AList.thy
     "[| P([]);   \
 \       !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)";

--- a/src/HOL/Subst/AList.thy	Mon May 15 17:30:19 2000 +0200
+++ b/src/HOL/Subst/AList.thy	Mon May 15 17:32:39 2000 +0200
@@ -9,14 +9,15 @@
 AList = List + 
 
 consts
-
   alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
   assoc      :: "['a,'b,('a*'b) list] => 'b"
 
-defs
+primrec
+  "alist_rec [] c d = c"
+  "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
 
-  alist_rec_def "alist_rec al b c == list_rec b (split c) al"
-
-  assoc_def   "assoc v d al == alist_rec al d (%x y xs g. if v=x then y else g)"
+primrec
+  "assoc v d [] = d"
+  "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
 
 end