--- a/src/Provers/blast.ML Fri Mar 06 22:06:33 2009 +0100
+++ b/src/Provers/blast.ML Fri Mar 06 23:25:08 2009 +0100
@@ -643,13 +643,13 @@
(*Print tracing information at each iteration of prover*)
fun tracing (State {thy, fullTrace, ...}) brs =
- let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm thy G)
- | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm thy H ^ "\t (Unsafe)")
+ let fun printPairs (((G,_)::_,_)::_) = Output.tracing (traceTerm thy G)
+ | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm thy H ^ "\t (Unsafe)")
| printPairs _ = ()
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
(fullTrace := brs0 :: !fullTrace;
- List.app (fn _ => Output.immediate_output "+") brs;
- Output.immediate_output (" [" ^ Int.toString lim ^ "] ");
+ List.app (fn _ => Output.tracing "+") brs;
+ Output.tracing (" [" ^ Int.toString lim ^ "] ");
printPairs pairs;
writeln"")
in if !trace then printBrs (map normBr brs) else ()
@@ -662,10 +662,10 @@
if !trace then
(case !ntrail-ntrl of
0 => ()
- | 1 => Output.immediate_output"\t1 variable UPDATED:"
- | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
+ | 1 => Output.tracing "\t1 variable UPDATED:"
+ | n => Output.tracing ("\t" ^ Int.toString n ^ " variables UPDATED:");
(*display the instantiations themselves, though no variable names*)
- List.app (fn v => Output.immediate_output(" " ^ string_of thy 4 (the (!v))))
+ List.app (fn v => Output.tracing (" " ^ string_of thy 4 (the (!v))))
(List.take(!trail, !ntrail-ntrl));
writeln"")
else ();
@@ -674,9 +674,9 @@
fun traceNew prems =
if !trace then
case length prems of
- 0 => Output.immediate_output"branch closed by rule"
- | 1 => Output.immediate_output"branch extended (1 new subgoal)"
- | n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
+ 0 => Output.tracing "branch closed by rule"
+ | 1 => Output.tracing "branch extended (1 new subgoal)"
+ | n => Output.tracing ("branch split: "^ Int.toString n ^ " new subgoals")
else ();
@@ -1005,7 +1005,7 @@
NONE => closeF Ls
| SOME tac =>
let val choices' =
- (if !trace then (Output.immediate_output"branch closed";
+ (if !trace then (Output.tracing "branch closed";
traceVars state ntrl)
else ();
prune state (nbrs, nxtVars,
@@ -1136,9 +1136,9 @@
clearTo state ntrl; raise NEWBRANCHES)
else
traceNew prems;
- if !trace andalso dup then Output.immediate_output" (duplicating)"
+ if !trace andalso dup then Output.tracing " (duplicating)"
else ();
- if !trace andalso recur then Output.immediate_output" (recursive)"
+ if !trace andalso recur then Output.tracing " (recursive)"
else ();
traceVars state ntrl;
if null prems then nclosed := !nclosed + 1
--- a/src/Pure/General/output.ML Fri Mar 06 22:06:33 2009 +0100
+++ b/src/Pure/General/output.ML Fri Mar 06 23:25:08 2009 +0100
@@ -32,7 +32,6 @@
val escape: output -> string
val std_output: output -> unit
val std_error: output -> unit
- val immediate_output: string -> unit
val writeln_default: output -> unit
val writeln_fn: (output -> unit) ref
val priority_fn: (output -> unit) ref
@@ -89,8 +88,6 @@
fun std_error s = NAMED_CRITICAL "IO" (fn () =>
(TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
-val immediate_output = std_output o output;
-
fun writeln_default "" = ()
| writeln_default s = std_output (suffix "\n" s);
--- a/src/Pure/Thy/thy_info.ML Fri Mar 06 22:06:33 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Mar 06 23:25:08 2009 +0100
@@ -383,7 +383,12 @@
fun schedule_seq tasks =
Graph.topological_order tasks
- |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () () | _ => ()));
+ |> List.app (fn name =>
+ (case Graph.get_node tasks name of
+ Task body =>
+ let val after_load = body ()
+ in after_load () handle exn => (kill_thy name; raise exn) end
+ | _ => ()));
in
--- a/src/Pure/Tools/find_theorems.ML Fri Mar 06 22:06:33 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Fri Mar 06 23:25:08 2009 +0100
@@ -168,8 +168,7 @@
fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
fun try_thm thm =
if Thm.no_prems thm then rtac thm 1 goal
- else (etacn thm THEN_ALL_NEW
- (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
+ else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
in
fn (_, thm) =>
if (is_some o Seq.pull o try_thm) thm
@@ -181,11 +180,10 @@
fun filter_simp ctxt t (_, thm) =
let
- val (_, {mk_rews = {mk, ...}, ...}) =
- Simplifier.rep_ss (Simplifier.local_simpset_of ctxt);
+ val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt);
val extract_simp =
- (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
- val ss = is_matching_thm extract_simp ctxt false t thm
+ (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
+ val ss = is_matching_thm extract_simp ctxt false t thm;
in
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
end;
--- a/src/Pure/meta_simplifier.ML Fri Mar 06 22:06:33 2009 +0100
+++ b/src/Pure/meta_simplifier.ML Fri Mar 06 23:25:08 2009 +0100
@@ -59,6 +59,7 @@
val delcongs: simpset * thm list -> simpset
val addsimprocs: simpset * simproc list -> simpset
val delsimprocs: simpset * simproc list -> simpset
+ val mksimps: simpset -> thm -> thm list
val setmksimps: simpset * (thm -> thm list) -> simpset
val setmkcong: simpset * (thm -> thm) -> simpset
val setmksym: simpset * (thm -> thm option) -> simpset
@@ -547,6 +548,7 @@
fun add_simp thm ss = ss addsimps [thm];
fun del_simp thm ss = ss delsimps [thm];
+
(* congs *)
fun cong_name (Const (a, _)) = SOME a
@@ -694,6 +696,8 @@
in
+val mksimps = #mk o #mk_rews o #2 o rep_ss;
+
fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
--- a/src/Tools/eqsubst.ML Fri Mar 06 22:06:33 2009 +0100
+++ b/src/Tools/eqsubst.ML Fri Mar 06 23:25:08 2009 +0100
@@ -128,8 +128,7 @@
(* changes object "=" to meta "==" which prepares a given rewrite rule *)
fun prep_meta_eq ctxt =
- let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
- in mk #> map Drule.zero_var_indexes end;
+ Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes;
(* a type abriviation for match information *)