# HG changeset patch
# User bulwahn
# Date 1284967578 -7200
# Node ID 9ff9651757cd1d5887658a8e3969098027b0bf99
# Parent  a50c0ae2312c789015055a2d4990121ebf9674bc
removing unnessary options for code_pred

diff -r a50c0ae2312c -r 9ff9651757cd src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Mon Sep 20 09:26:16 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Mon Sep 20 09:26:18 2010 +0200
@@ -1612,13 +1612,13 @@
   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}"