diff -r 95f66b234086 -r 9a1178204dc0 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Apr 22 11:10:23 2009 +0200
+++ b/src/HOL/Predicate.thy	Mon May 11 09:18:42 2009 +0200
@@ -640,4 +640,12 @@
 hide (open) const Pred eval single bind if_pred not_pred
   Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
 
+text {* dummy setup for code_pred keyword *}
+
+ML {*
+OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
+  OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]])))
+*}
+
+
 end