src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -6,9 +6,10 @@
 
 signature PREDICATE_COMPILE_CORE =
 sig
-  val setup: theory -> theory
-  val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
-  val code_pred_cmd: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+  val setup : theory -> theory
+  val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+  val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+  val values_cmd : string list -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
   val register_predicate : (string * thm list * thm * int) -> theory -> theory
   val register_intros : string * thm list -> theory -> theory
   val is_registered : theory -> string -> bool
@@ -23,13 +24,13 @@
   val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
   val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
   val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
-  val intros_of: theory -> string -> thm list
-  val nparams_of: theory -> string -> int
-  val add_intro: thm -> theory -> theory
-  val set_elim: thm -> theory -> theory
+  val intros_of : theory -> string -> thm list
+  val nparams_of : theory -> string -> int
+  val add_intro : thm -> theory -> theory
+  val set_elim : thm -> theory -> theory
   val set_nparams : string -> int -> theory -> theory
-  val print_stored_rules: theory -> unit
-  val print_all_modes: theory -> unit
+  val print_stored_rules : theory -> unit
+  val print_all_modes : theory -> unit
   val mk_casesrule : Proof.context -> term -> int -> thm list -> term
   val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
   val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref
@@ -2564,37 +2565,16 @@
   in
   end;
   *)
-fun values_cmd modes options k raw_t state =
+fun values_cmd print_modes options k raw_t state =
   let
     val ctxt = Toplevel.context_of state;
     val t = Syntax.read_term ctxt raw_t;
     val t' = values ctxt options k t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
+    val p = PrintMode.with_modes print_modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
 
-local structure P = OuterParse in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-val options =
-  let
-    val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
-    val random = Scan.optional (Args.$$$ "random" >> K true) false
-    val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false
-  in
-    Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]")
-      (NONE, (false, false))
-  end
-
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
-  (opt_modes -- options -- Scan.optional P.nat ~1 -- P.term
-    >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep
-        (values_cmd modes options k t)));
-
 end;
-
-end;