# HG changeset patch
# User bulwahn
# Date 1258013437 -3600
# Node ID 24a91a380ee32f1fe826c0b6448517a1331081b9
# Parent  dd564a26fd2f7213a67a23b96de37091608e357d
removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main

diff -r dd564a26fd2f -r 24a91a380ee3 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Nov 12 09:10:30 2009 +0100
+++ b/src/HOL/Predicate.thy	Thu Nov 12 09:10:37 2009 +0100
@@ -828,28 +828,6 @@
 
 code_abort not_unique
 
-text {* dummy setup for @{text code_pred} and @{text values} keywords *}
-
-ML {*
-local
-
-structure P = OuterParse;
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-in
-
-val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
-  OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]])));
-
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions"
-  OuterKeyword.diag ((opt_modes -- P.term)
-    >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep
-        (K ())));
-
-end
-*}
-
 no_notation
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and