1.1 --- a/src/HOL/Library/AssocList.thy	Tue Feb 26 20:38:16 2008 +0100
     1.2 +++ b/src/HOL/Library/AssocList.thy	Tue Feb 26 20:38:17 2008 +0100
     1.3 @@ -16,29 +16,27 @@
     1.4    to establish the invariant, e.g. for inductive proofs.
     1.5  *}
     1.6  
     1.7 -fun
     1.8 +primrec
     1.9    delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.10  where
    1.11      "delete k [] = []"
    1.12    | "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
    1.13  
    1.14 -fun
    1.15 +primrec
    1.16    update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.17  where
    1.18      "update k v [] = [(k, v)]"
    1.19    | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    1.20  
    1.21 -function
    1.22 +primrec
    1.23    updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.24  where
    1.25      "updates [] vs ps = ps"
    1.26    | "updates (k#ks) vs ps = (case vs
    1.27        of [] \<Rightarrow> ps
    1.28         | (v#vs') \<Rightarrow> updates ks vs' (update k v ps))"
    1.29 -by pat_completeness auto
    1.30 -termination by lexicographic_order
    1.31  
    1.32 -fun
    1.33 +primrec
    1.34    merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.35  where
    1.36      "merge qs [] = qs"
    1.37 @@ -66,23 +64,21 @@
    1.38    finally show ?thesis .
    1.39  qed
    1.40  
    1.41 -function
    1.42 +fun
    1.43    compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
    1.44  where
    1.45      "compose [] ys = []"
    1.46    | "compose (x#xs) ys = (case map_of ys (snd x)
    1.47         of None \<Rightarrow> compose (delete (fst x) xs) ys
    1.48          | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
    1.49 -by pat_completeness auto
    1.50 -termination by lexicographic_order
    1.51  
    1.52 -fun
    1.53 +primrec
    1.54    restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.55  where
    1.56      "restrict A [] = []"
    1.57    | "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
    1.58  
    1.59 -fun
    1.60 +primrec
    1.61    map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.62  where
    1.63      "map_ran f [] = []"

     2.1 --- a/src/HOL/Library/Char_nat.thy	Tue Feb 26 20:38:16 2008 +0100
     2.2 +++ b/src/HOL/Library/Char_nat.thy	Tue Feb 26 20:38:17 2008 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4  
     2.5  text {* Conversions between nibbles and natural numbers in [0..15]. *}
     2.6  
     2.7 -fun
     2.8 +primrec
     2.9    nat_of_nibble :: "nibble \<Rightarrow> nat" where
    2.10      "nat_of_nibble Nibble0 = 0"
    2.11    | "nat_of_nibble Nibble1 = 1"
    2.12 @@ -119,7 +119,7 @@
    2.13    "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
    2.14    unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
    2.15  
    2.16 -fun
    2.17 +primrec
    2.18    nat_of_char :: "char \<Rightarrow> nat" where
    2.19    "nat_of_char (Char n m) = nat_of_nibble n * 16 + nat_of_nibble m"
    2.20