--- a/doc-src/Codegen/Thy/ML.thy Mon Nov 16 10:16:40 2009 +0100
+++ b/doc-src/Codegen/Thy/ML.thy Mon Nov 16 11:14:43 2009 +0100
@@ -24,7 +24,6 @@
\begin{mldecls}
@{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
@{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
- @{index_ML Code.add_eqnl: "string * (thm * bool) list lazy -> theory -> theory"} \\
@{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
@{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
@{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
@@ -44,10 +43,6 @@
\item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
theorem @{text "thm"} from executable content, if present.
- \item @{ML Code.add_eqnl}~@{text "(const, lthms)"}~@{text "thy"} adds
- suspended code equations @{text lthms} for constant
- @{text const} to executable content.
-
\item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
the preprocessor simpset.
--- a/doc-src/Codegen/Thy/Program.thy Mon Nov 16 10:16:40 2009 +0100
+++ b/doc-src/Codegen/Thy/Program.thy Mon Nov 16 11:14:43 2009 +0100
@@ -356,47 +356,8 @@
For datatypes, instances of @{class eq} are implicitly derived
when possible. For other types, you may instantiate @{text eq}
manually like any other type class.
-
- Though this @{text eq} class is designed to get rarely in
- the way, in some cases the automatically derived code equations
- for equality on a particular type may not be appropriate.
- As example, watch the following datatype representing
- monomorphic parametric types (where type constructors
- are referred to by natural numbers):
*}
-datatype %quote monotype = Mono nat "monotype list"
-(*<*)
-lemma monotype_eq:
- "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<equiv>
- eq_class.eq tyco1 tyco2 \<and> eq_class.eq typargs1 typargs2" by (simp add: eq)
-(*>*)
-
-text {*
- \noindent Then code generation for SML would fail with a message
- that the generated code contains illegal mutual dependencies:
- the theorem @{thm monotype_eq [no_vars]} already requires the
- instance @{text "monotype \<Colon> eq"}, which itself requires
- @{thm monotype_eq [no_vars]}; Haskell has no problem with mutually
- recursive @{text instance} and @{text function} definitions,
- but the SML serialiser does not support this.
-
- In such cases, you have to provide your own equality equations
- involving auxiliary constants. In our case,
- @{const [show_types] list_all2} can do the job:
-*}
-
-lemma %quote monotype_eq_list_all2 [code]:
- "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
- eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
- by (simp add: eq list_all2_eq [symmetric])
-
-text {*
- \noindent does not depend on instance @{text "monotype \<Colon> eq"}:
-*}
-
-text %quote {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
-
subsection {* Explicit partiality *}
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Mon Nov 16 10:16:40 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Mon Nov 16 11:14:43 2009 +0100
@@ -236,10 +236,10 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype boola = True | False;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun anda x True = x\\
-\hspace*{0pt} ~| anda x False = False\\
-\hspace*{0pt} ~| anda True x = x\\
-\hspace*{0pt} ~| anda False x = False;\\
+\hspace*{0pt}fun anda p True = p\\
+\hspace*{0pt} ~| anda p False = False\\
+\hspace*{0pt} ~| anda True p = p\\
+\hspace*{0pt} ~| anda False p = False;\\
\hspace*{0pt}\\
\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
--- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Nov 16 10:16:40 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Mon Nov 16 11:14:43 2009 +0100
@@ -160,7 +160,7 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
\hspace*{0pt}\\
\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
--- a/doc-src/Codegen/Thy/document/ML.tex Mon Nov 16 10:16:40 2009 +0100
+++ b/doc-src/Codegen/Thy/document/ML.tex Mon Nov 16 11:14:43 2009 +0100
@@ -54,7 +54,6 @@
\begin{mldecls}
\indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
\indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
- \indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
@@ -74,10 +73,6 @@
\item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
theorem \isa{thm} from executable content, if present.
- \item \verb|Code.add_eqnl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
- suspended code equations \isa{lthms} for constant
- \isa{const} to executable content.
-
\item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
the preprocessor simpset.
--- a/doc-src/Codegen/Thy/document/Program.tex Mon Nov 16 10:16:40 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex Mon Nov 16 11:14:43 2009 +0100
@@ -356,7 +356,7 @@
\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
\hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\
+\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
\hspace*{0pt}\\
\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
@@ -667,7 +667,7 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
\hspace*{0pt}\\
\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
@@ -797,124 +797,10 @@
\isa{eq} constraints through all dependent code equations.
For datatypes, instances of \isa{eq} are implicitly derived
when possible. For other types, you may instantiate \isa{eq}
- manually like any other type class.
-
- Though this \isa{eq} class is designed to get rarely in
- the way, in some cases the automatically derived code equations
- for equality on a particular type may not be appropriate.
- As example, watch the following datatype representing
- monomorphic parametric types (where type constructors
- are referred to by natural numbers):%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{datatype}\isamarkupfalse%
-\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent Then code generation for SML would fail with a message
- that the generated code contains illegal mutual dependencies:
- the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the
- instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
- \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually
- recursive \isa{instance} and \isa{function} definitions,
- but the SML serialiser does not support this.
-
- In such cases, you have to provide your own equality equations
- involving auxiliary constants. In our case,
- \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
+ manually like any other type class.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
-\ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun null [] = true\\
-\hspace*{0pt} ~| null (x ::~xs) = false;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun eq{\char95}nat (Suc nat') Zero{\char95}nat = false\\
-\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc nat') = false\\
-\hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
-\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\
-\hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
-\hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\
-\hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
\isamarkupsubsection{Explicit partiality%
}
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/examples/example.ML Mon Nov 16 10:16:40 2009 +0100
+++ b/doc-src/Codegen/Thy/examples/example.ML Mon Nov 16 11:14:43 2009 +0100
@@ -11,7 +11,7 @@
datatype 'a queue = AQueue of 'a list * 'a list;
-val empty : 'a queue = AQueue ([], [])
+val empty : 'a queue = AQueue ([], []);
fun dequeue (AQueue ([], [])) = (NONE, AQueue ([], []))
| dequeue (AQueue (xs, y :: ys)) = (SOME y, AQueue (xs, ys))
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 16 10:16:40 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 16 11:14:43 2009 +0100
@@ -7,6 +7,7 @@
signature NITPICK =
sig
+ type styp = Nitpick_Util.styp
type params = {
cards_assigns: (typ option * int list) list,
maxes_assigns: (styp option * int list) list,
@@ -231,9 +232,8 @@
else
neg_t
val (assms_t, evals) =
- assms_t :: evals
- |> merge_type_vars ? merge_type_vars_in_terms
- |> hd pairf tl
+ assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms
+ |> pairf hd tl
val original_max_potential = max_potential
val original_max_genuine = max_genuine
(*
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Nov 16 10:16:40 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Nov 16 11:14:43 2009 +0100
@@ -7,6 +7,7 @@
signature NITPICK_HOL =
sig
+ type styp = Nitpick_Util.styp
type const_table = term list Symtab.table
type special_fun = (styp * int list * term list) * styp
type unrolled = styp * styp
@@ -1499,7 +1500,7 @@
SOME n =>
let
val (dataT, res_T) = nth_range_type n T
- |> domain_type pairf range_type
+ |> pairf domain_type range_type
in
(optimized_case_def ext_ctxt dataT res_T
|> do_term (depth + 1) Ts, ts)
@@ -1675,8 +1676,8 @@
| NONE =>
let
val goal = prop |> cterm_of thy |> Goal.init
- val wf = silence (exists (terminates_by ctxt tac_timeout goal))
- termination_tacs
+ val wf = exists (terminates_by ctxt tac_timeout goal)
+ termination_tacs
in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
end)
handle List.Empty => false
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Nov 16 10:16:40 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Nov 16 11:14:43 2009 +0100
@@ -216,7 +216,7 @@
("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +))
else if Kodkod.Rel x = nat_subtract_rel then
("nat_subtract",
- tabulate_op2 debug univ_card (nat_card, j0) j0 (op nat_minus))
+ tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus))
else if Kodkod.Rel x = int_subtract_rel then
("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -))
else if Kodkod.Rel x = nat_multiply_rel then
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Nov 16 10:16:40 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Nov 16 11:14:43 2009 +0100
@@ -7,6 +7,7 @@
signature NITPICK_MODEL =
sig
+ type styp = Nitpick_Util.styp
type scope = Nitpick_Scope.scope
type rep = Nitpick_Rep.rep
type nut = Nitpick_Nut.nut
@@ -636,7 +637,7 @@
||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of)
val free_names =
map (fn x as (s, T) =>
- case filter (equal x o nickname_of pairf (unbox_type o type_of))
+ case filter (equal x o pairf nickname_of (unbox_type o type_of))
free_names of
[name] => name
| [] => FreeName (s, T, Any)
@@ -698,8 +699,8 @@
| TimeLimit.TimeOut => false
end
in
- if silence try_out false then SOME true
- else if silence try_out true then SOME false
+ if try_out false then SOME true
+ else if try_out true then SOME false
else NONE
end
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Nov 16 10:16:40 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Nov 16 11:14:43 2009 +0100
@@ -531,7 +531,7 @@
| _ => raise SAME ()
else if r22 = nat_subtract_rel then
case (r21, r1) of
- (Atom j1, Atom j2) => from_nat (to_nat j1 nat_minus to_nat j2)
+ (Atom j1, Atom j2) => from_nat (nat_minus (to_nat j1) (to_nat j2))
| _ => raise SAME ()
else if r22 = nat_multiply_rel then
case (r21, r1) of
@@ -581,11 +581,11 @@
let
val arity2 = arity_of_rel_expr r2
val arity1 = arity - arity2
- val n1 = Int.min (arity1 nat_minus j0, n)
+ val n1 = Int.min (nat_minus arity1 j0, n)
val n2 = n - n1
(* unit -> rel_expr *)
fun one () = aux arity1 r1 j0 n1
- fun two () = aux arity2 r2 (j0 nat_minus arity1) n2
+ fun two () = aux arity2 r2 (nat_minus j0 arity1) n2
in
case (n1, n2) of
(0, _) => s_rel_if (s_some r1) (two ()) (empty_n_ary_rel n2)
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Nov 16 10:16:40 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Nov 16 11:14:43 2009 +0100
@@ -7,6 +7,7 @@
signature NITPICK_SCOPE =
sig
+ type styp = Nitpick_Util.styp
type extended_context = Nitpick_HOL.extended_context
type constr_spec = {
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Nov 16 10:16:40 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Nov 16 11:14:43 2009 +0100
@@ -5,18 +5,9 @@
General-purpose functions used by the Nitpick modules.
*)
-infix 6 nat_minus
-infix 7 pairf
-
-signature BASIC_NITPICK_UTIL =
+signature NITPICK_UTIL =
sig
type styp = string * typ
-end;
-
-signature NITPICK_UTIL =
-sig
- include BASIC_NITPICK_UTIL
-
datatype polarity = Pos | Neg | Neut
exception ARG of string * string
@@ -27,9 +18,9 @@
val nitpick_prefix : string
val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
- val pairf : ('a -> 'b) * ('a -> 'c) -> 'a -> 'b * 'c
+ val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
val int_for_bool : bool -> int
- val nat_minus : int * int -> int
+ val nat_minus : int -> int -> int
val reasonable_power : int -> int -> int
val exact_log : int -> int -> int
val exact_root : int -> int -> int
@@ -63,7 +54,6 @@
val subscript : string -> string
val nat_subscript : int -> string
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
- val silence : ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
val indent_size : int
@@ -90,13 +80,13 @@
(* ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd *)
fun curry3 f = fn x => fn y => fn z => f (x, y, z)
-(* ('a -> 'b) * ('a -> 'c) -> 'a -> 'b * 'c *)
-fun (f pairf g) = fn x => (f x, g x)
+(* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *)
+fun pairf f g x = (f x, g x)
(* bool -> int *)
fun int_for_bool b = if b then 1 else 0
-(* int * int -> int *)
-fun (i nat_minus j) = if i > j then i - j else 0
+(* int -> int -> int *)
+fun nat_minus i j = if i > j then i - j else 0
val max_exponent = 16384
@@ -263,15 +253,6 @@
fun time_limit NONE f = f
| time_limit (SOME delay) f = TimeLimit.timeLimit delay f
-(* (string -> unit) Unsynchronized.ref -> ('a -> 'b) -> 'a -> 'b *)
-fun silence_one out_fn = setmp_CRITICAL out_fn (K ())
-
-(* ('a -> 'b) -> 'a -> 'b *)
-fun silence f =
- fold silence_one
- [Output.writeln_fn, Output.priority_fn, Output.tracing_fn,
- Output.warning_fn, Output.error_fn, Output.debug_fn] f
-
(* Time.time option -> tactic -> tactic *)
fun DETERM_TIMEOUT delay tac st =
Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
@@ -302,6 +283,3 @@
end
end;
-
-structure Basic_Nitpick_Util : BASIC_NITPICK_UTIL = Nitpick_Util;
-open Basic_Nitpick_Util;