src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy

 ({ rule ''S'' [NTS ''A'', NTS ''B''],
    rule ''S'' [TS ''a''],
   rule ''A'' [TS ''b'']}, ''S'')"
 
 
-code_pred [inductify,skip_proof] derives .
+code_pred [inductify, skip_proof] derives .
 
 thm derives.equation
 
 definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }"
 
-code_pred (modes: o \<Rightarrow> bool) [inductify, show_modes, show_intermediate_results, skip_proof] test .
+code_pred (modes: o \<Rightarrow> bool) [inductify] test .
 thm test.equation
 
 values "{rhs. test rhs}"
 
 declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def]