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