src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy

 code_pred [random_dseq] filter2 .
 
 thm filter2.equation
 thm filter2.random_dseq_equation
 
-(*
 inductive filter3
 for P
 where
   "List.filter P xs = ys ==> filter3 P xs ys"
 
 code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 .
 
-code_pred [dseq] filter3 .
-thm filter3.dseq_equation
-*)
+code_pred filter3 .
+thm filter3.equation
+
 (*
 inductive filter4
 where
   "List.filter P xs = ys ==> filter4 P xs ys"