src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy

 definition
   "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
 
 code_pred [inductify, skip_proof] case_f .
 thm case_fP.equation
-thm case_fP.intros
 
 fun fold_map_idx where
   "fold_map_idx f i y [] = (y, [])"
 | "fold_map_idx f i y (x # xs) =
  (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs

   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
 (*
 code_pred [inductify] avl .
 thm avl.equation*)
 
-code_pred [random_dseq inductify] avl .
-thm avl.random_dseq_equation
-
-values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
+code_pred [new_random_dseq inductify] avl .
+thm avl.new_random_dseq_equation
+
+values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
 
 fun set_of
 where
 "set_of ET = {}"
 | "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"