1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
     1.3 @@ -810,8 +810,7 @@
     1.4   (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
     1.5   in (y'', x' # xs'))"
     1.6  
     1.7 -text {* mode analysis explores thousand modes - this is infeasible at the moment... *}
     1.8 -(*code_pred [inductify, show_steps] fold_map_idx .*)
     1.9 +code_pred [inductify] fold_map_idx .
    1.10  
    1.11  subsection {* Minimum *}
    1.12  
    1.13 @@ -939,10 +938,10 @@
    1.14  "height ET = 0"
    1.15  | "height (MKT x l r h) = max (height l) (height r) + 1"
    1.16  
    1.17 -consts avl :: "'a tree => bool"
    1.18 -primrec
    1.19 +primrec avl :: "'a tree => bool"
    1.20 +where
    1.21    "avl ET = True"
    1.22 -  "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
    1.23 +| "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
    1.24    h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
    1.25  (*
    1.26  code_pred [inductify] avl .