removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
authorbulwahn
Thu, 12 Nov 2009 09:10:37 +0100
changeset 33622 24a91a380ee3
parent 33621 dd564a26fd2f
child 33623 4ec42d38224f
removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
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