--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Aug 27 18:00:45 2010 +0200
@@ -5,11 +5,11 @@
val tests = ["Brackin", "Instructions", "SML", "Verilog"];
-Unsynchronized.set timing;
+timing := true;
-warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
+warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
use_thys tests;
-warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
+warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
List.app Thy_Info.remove_thy tests;
use_thys tests;
--- a/Admin/Benchmarks/HOL-record/ROOT.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/Admin/Benchmarks/HOL-record/ROOT.ML Fri Aug 27 18:00:45 2010 +0200
@@ -5,10 +5,10 @@
val tests = ["RecordBenchmark"];
-Unsynchronized.set timing;
+timing := true;
-warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
+warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
use_thys tests;
-warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
+warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
use_thys tests;
--- a/Admin/Benchmarks/HOL-record/RecordBenchmark.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/Admin/Benchmarks/HOL-record/RecordBenchmark.thy Fri Aug 27 18:00:45 2010 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-ML {* Unsynchronized.set Record.timing *}
+ML {* Record.timing := true *}
record many_A =
A000::nat
--- a/NEWS Fri Aug 27 16:05:46 2010 +0200
+++ b/NEWS Fri Aug 27 18:00:45 2010 +0200
@@ -39,6 +39,12 @@
Note that the corresponding "..._default" references may be only
changed globally at the ROOT session setup, but *not* within a theory.
+* ML structure Unsynchronized never opened, not even in Isar
+interaction mode as before. Old Unsynchronized.set etc. have been
+discontinued -- use plain := instead. This should be *rare* anyway,
+since modern tools always work via official context data, notably
+configuration options.
+
*** Pure ***
--- a/doc-src/Codegen/Thy/Setup.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Fri Aug 27 18:00:45 2010 +0200
@@ -27,6 +27,6 @@
setup {* Code_Target.set_default_code_width 74 *}
-ML_command {* Unsynchronized.reset unique_names *}
+ML_command {* unique_names := false *}
end
--- a/doc-src/IsarOverview/Isar/ROOT.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/doc-src/IsarOverview/Isar/ROOT.ML Fri Aug 27 18:00:45 2010 +0200
@@ -1,3 +1,3 @@
-Unsynchronized.set quick_and_dirty;
+quick_and_dirty := true;
use_thys ["Logic", "Induction"];
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Aug 27 18:00:45 2010 +0200
@@ -132,7 +132,7 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{quote}
-@{ML "Unsynchronized.reset show_question_marks"}\verb!;!
+@{ML "show_question_marks := false"}\verb!;!
\end{quote}
at the beginning of your file \texttt{ROOT.ML}.
The rest of this document is produced with this flag set to \texttt{false}.
@@ -144,7 +144,7 @@
turning the last digit into a subscript: write \verb!x\<^isub>1! and
obtain the much nicer @{text"x\<^isub>1"}. *}
-(*<*)ML "Unsynchronized.reset show_question_marks"(*>*)
+(*<*)ML "show_question_marks := false"(*>*)
subsection {*Qualified names*}
@@ -155,7 +155,7 @@
short names (no qualifiers) by setting \verb!short_names!, typically
in \texttt{ROOT.ML}:
\begin{quote}
-@{ML "Unsynchronized.set short_names"}\verb!;!
+@{ML "short_names := true"}\verb!;!
\end{quote}
*}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Aug 27 16:05:46 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Aug 27 18:00:45 2010 +0200
@@ -173,7 +173,7 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{quote}
-\verb|Unsynchronized.reset show_question_marks|\verb!;!
+\verb|show_question_marks := false|\verb!;!
\end{quote}
at the beginning of your file \texttt{ROOT.ML}.
The rest of this document is produced with this flag set to \texttt{false}.
@@ -211,7 +211,7 @@
short names (no qualifiers) by setting \verb!short_names!, typically
in \texttt{ROOT.ML}:
\begin{quote}
-\verb|Unsynchronized.set short_names|\verb!;!
+\verb|short_names := true|\verb!;!
\end{quote}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Misc/Itrev.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Fri Aug 27 18:00:45 2010 +0200
@@ -2,7 +2,7 @@
theory Itrev
imports Main
begin
-ML"Unsynchronized.reset unique_names"
+ML"unique_names := false"
(*>*)
section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
\index{induction heuristics|)}
*}
(*<*)
-ML"Unsynchronized.set unique_names"
+ML"unique_names := true"
end
(*>*)
--- a/doc-src/TutorialI/Rules/Basic.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy Fri Aug 27 18:00:45 2010 +0200
@@ -187,7 +187,7 @@
text{*unification failure trace *}
-ML "Unsynchronized.set trace_unify_fail"
+ML "trace_unify_fail := true"
lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"
txt{*
@@ -212,7 +212,7 @@
*}
oops
-ML "Unsynchronized.reset trace_unify_fail"
+ML "trace_unify_fail := false"
text{*Quantifiers*}
--- a/doc-src/TutorialI/Sets/Examples.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy Fri Aug 27 18:00:45 2010 +0200
@@ -1,7 +1,6 @@
-(* ID: $Id$ *)
theory Examples imports Main Binomial begin
-ML "Unsynchronized.reset eta_contract"
+ML "eta_contract := false"
ML "Pretty.margin_default := 64"
text{*membership, intersection *}
--- a/src/CCL/ROOT.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/CCL/ROOT.ML Fri Aug 27 18:00:45 2010 +0200
@@ -8,6 +8,6 @@
evaluation to weak head-normal form.
*)
-Unsynchronized.set eta_contract;
+eta_contract := true;
use_thys ["Wfd", "Fix"];
--- a/src/FOLP/IFOLP.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/src/FOLP/IFOLP.thy Fri Aug 27 18:00:45 2010 +0200
@@ -63,20 +63,22 @@
syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5)
-ML {*
-
-(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
-val show_proofs = Unsynchronized.ref false;
-
-fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
-
-fun proof_tr' [P,p] =
- if ! show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
- else P (*this case discards the proof term*);
+parse_translation {*
+ let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p
+ in [(@{syntax_const "_Proof"}, proof_tr)] end
*}
-parse_translation {* [(@{syntax_const "_Proof"}, proof_tr)] *}
-print_translation {* [(@{const_syntax Proof}, proof_tr')] *}
+(*show_proofs = true displays the proof terms -- they are ENORMOUS*)
+ML {* val (show_proofs, setup_show_proofs) = Attrib.config_bool "show_proofs" (K false) *}
+setup setup_show_proofs
+
+print_translation (advanced) {*
+ let
+ fun proof_tr' ctxt [P, p] =
+ if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
+ else P
+ in [(@{const_syntax Proof}, proof_tr')] end
+*}
axioms
--- a/src/HOL/Import/import_syntax.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Import/import_syntax.ML Fri Aug 27 18:00:45 2010 +0200
@@ -148,11 +148,11 @@
val _ = TextIO.closeIn is
val orig_source = Source.of_string inp
val symb_source = Symbol.source {do_recover = false} orig_source
- val lexes = Unsynchronized.ref
- (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
+ val lexes =
+ (Scan.make_lexicon
+ (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
Scan.empty_lexicon)
- val get_lexes = fn () => !lexes
- val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
+ val token_source = Token.source {do_recover = NONE} (K lexes) Position.start symb_source
val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
val type_mapsP = Parse.$$$ "type_maps" |-- type_maps
--- a/src/HOL/Library/Sum_Of_Squares.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy Fri Aug 27 18:00:45 2010 +0200
@@ -28,6 +28,7 @@
without calling an external prover.
*}
+setup Sum_Of_Squares.setup
setup SOS_Wrapper.setup
text {* Tests *}
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Fri Aug 27 18:00:45 2010 +0200
@@ -8,8 +8,8 @@
sig
datatype prover_result = Success | Failure | Error
val setup: theory -> theory
- val destdir: string Unsynchronized.ref
- val prover_name: string Unsynchronized.ref
+ val dest_dir: string Config.T
+ val prover_name: string Config.T
end
structure SOS_Wrapper: SOS_WRAPPER =
@@ -22,14 +22,9 @@
| str_of_result Error = "Error"
-(*** output control ***)
-
-fun debug s = if ! Sum_Of_Squares.debugging then writeln s else ()
-
-
(*** calling provers ***)
-val destdir = Unsynchronized.ref ""
+val (dest_dir, setup_dest_dir) = Attrib.config_string "sos_dest_dir" (K "")
fun filename dir name =
let
@@ -43,12 +38,12 @@
else error ("No such directory: " ^ dir)
end
-fun run_solver name cmd find_failure input =
+fun run_solver ctxt name cmd find_failure input =
let
val _ = warning ("Calling solver: " ^ name)
(* create input file *)
- val dir = ! destdir
+ val dir = Config.get ctxt dest_dir
val input_file = filename dir "sos_in"
val _ = File.write input_file input
@@ -71,7 +66,10 @@
(File.rm input_file; if File.exists output_file then File.rm output_file else ())
else ()
- val _ = debug ("Solver output:\n" ^ output)
+ val _ =
+ if Config.get ctxt Sum_Of_Squares.trace
+ then writeln ("Solver output:\n" ^ output)
+ else ()
val _ = warning (str_of_result res ^ ": " ^ res_msg)
in
@@ -120,13 +118,13 @@
| prover "csdp" = csdp
| prover name = error ("Unknown prover: " ^ name)
-val prover_name = Unsynchronized.ref "remote_csdp"
+val (prover_name, setup_prover_name) = Attrib.config_string "sos_prover_name" (K "remote_csdp")
-fun call_solver opt_name =
+fun call_solver ctxt opt_name =
let
- val name = the_default (! prover_name) opt_name
+ val name = the_default (Config.get ctxt prover_name) opt_name
val (cmd, find_failure) = prover name
- in run_solver name (Path.explode cmd) find_failure end
+ in run_solver ctxt name (Path.explode cmd) find_failure end
(* certificate output *)
@@ -143,9 +141,13 @@
fun sos_solver print method = SIMPLE_METHOD' o Sum_Of_Squares.sos_tac print method
val setup =
+ setup_dest_dir #>
+ setup_prover_name #>
Method.setup @{binding sos}
(Scan.lift (Scan.option Parse.xname)
- >> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
+ >> (fn opt_name => fn ctxt =>
+ sos_solver print_cert
+ (Sum_Of_Squares.Prover (call_solver ctxt opt_name)) ctxt))
"prove universal problems over the reals using sums of squares" #>
Method.setup @{binding sos_cert}
(Scan.lift Parse.string
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 18:00:45 2010 +0200
@@ -9,7 +9,8 @@
sig
datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
- val debugging: bool Unsynchronized.ref
+ val trace: bool Config.T
+ val setup: theory -> theory
exception Failure of string;
end
@@ -49,7 +50,8 @@
val pow2 = rat_pow rat_2;
val pow10 = rat_pow rat_10;
-val debugging = Unsynchronized.ref false;
+val (trace, setup_trace) = Attrib.config_bool "sos_trace" (K false);
+val setup = setup_trace;
exception Sanity;
@@ -1059,7 +1061,7 @@
(* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
-fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
+fun real_positivnullstellensatz_general ctxt prover linf d eqs leqs pol =
let
val vars = fold_rev (union (op aconvc) o poly_variables)
(pol :: eqs @ map fst leqs) []
@@ -1129,7 +1131,7 @@
fun find_rounding d =
let
val _ =
- if !debugging
+ if Config.get ctxt trace
then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
else ()
val vec = nice_vector d raw_vec
@@ -1245,7 +1247,7 @@
let val e = multidegree pol
val k = if e = 0 then 0 else d div e
val eq' = map fst eq
- in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
+ in tryfind (fn i => (d,i,real_positivnullstellensatz_general ctxt prover false d eq' leq
(poly_neg(poly_pow pol i))))
(0 upto k)
end
--- a/src/HOL/Library/positivstellensatz.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Fri Aug 27 18:00:45 2010 +0200
@@ -164,21 +164,6 @@
thm list * thm list * thm list -> thm * pss_tree
type cert_conv = cterm -> thm * pss_tree
-val my_eqs = Unsynchronized.ref ([] : thm list);
-val my_les = Unsynchronized.ref ([] : thm list);
-val my_lts = Unsynchronized.ref ([] : thm list);
-val my_proof = Unsynchronized.ref (Axiom_eq 0);
-val my_context = Unsynchronized.ref @{context};
-
-val my_mk_numeric = Unsynchronized.ref ((K @{cterm True}) :Rat.rat -> cterm);
-val my_numeric_eq_conv = Unsynchronized.ref no_conv;
-val my_numeric_ge_conv = Unsynchronized.ref no_conv;
-val my_numeric_gt_conv = Unsynchronized.ref no_conv;
-val my_poly_conv = Unsynchronized.ref no_conv;
-val my_poly_neg_conv = Unsynchronized.ref no_conv;
-val my_poly_add_conv = Unsynchronized.ref no_conv;
-val my_poly_mul_conv = Unsynchronized.ref no_conv;
-
(* Some useful derived rules *)
fun deduct_antisym_rule tha thb =
@@ -362,11 +347,6 @@
poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
absconv1,absconv2,prover) =
let
- val _ = my_context := ctxt
- val _ = (my_mk_numeric := mk_numeric ; my_numeric_eq_conv := numeric_eq_conv ;
- my_numeric_ge_conv := numeric_ge_conv; my_numeric_gt_conv := numeric_gt_conv ;
- my_poly_conv := poly_conv; my_poly_neg_conv := poly_neg_conv;
- my_poly_add_conv := poly_add_conv; my_poly_mul_conv := poly_mul_conv)
val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}]
val prenex_ss = HOL_basic_ss addsimps prenex_simps
val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
@@ -408,7 +388,6 @@
fun hol_of_positivstellensatz(eqs,les,lts) proof =
let
- val _ = (my_eqs := eqs ; my_les := les ; my_lts := lts ; my_proof := proof)
fun translate prf = case prf of
Axiom_eq n => nth eqs n
| Axiom_le n => nth les n
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Aug 27 18:00:45 2010 +0200
@@ -371,7 +371,7 @@
fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
val (_, export_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) =>
+ (Thm.add_oracle (@{binding compute}, fn (thy, hyps, shyps, prop) =>
let
val shyptab = add_shyps shyps Sorttab.empty
fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
--- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Aug 27 18:00:45 2010 +0200
@@ -18,8 +18,6 @@
val eqvt_force_del: attribute
val setup: theory -> theory
val get_eqvt_thms: Proof.context -> thm list
-
- val NOMINAL_EQVT_DEBUG : bool Unsynchronized.ref
end;
structure NominalThmDecls: NOMINAL_THMDECLS =
@@ -44,29 +42,31 @@
(* equality-lemma can be derived. *)
exception EQVT_FORM of string
-val NOMINAL_EQVT_DEBUG = Unsynchronized.ref false
+val (nominal_eqvt_debug, setup_nominal_eqvt_debug) =
+ Attrib.config_bool "nominal_eqvt_debug" (K false);
-fun tactic (msg, tac) =
- if !NOMINAL_EQVT_DEBUG
+fun tactic ctxt (msg, tac) =
+ if Config.get ctxt nominal_eqvt_debug
then tac THEN' (K (print_tac ("after " ^ msg)))
else tac
fun prove_eqvt_tac ctxt orig_thm pi pi' =
-let
- val mypi = Thm.cterm_of ctxt pi
- val T = fastype_of pi'
- val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
- val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp"
-in
- EVERY1 [tactic ("iffI applied", rtac @{thm iffI}),
- tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
- tactic ("solve with orig_thm", etac orig_thm),
- tactic ("applies orig_thm instantiated with rev pi",
- dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
- tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
- tactic ("getting rid of all remaining perms",
- full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
-end;
+ let
+ val thy = ProofContext.theory_of ctxt
+ val mypi = Thm.cterm_of thy pi
+ val T = fastype_of pi'
+ val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
+ val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"
+ in
+ EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}),
+ tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
+ tactic ctxt ("solve with orig_thm", etac orig_thm),
+ tactic ctxt ("applies orig_thm instantiated with rev pi",
+ dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
+ tactic ctxt ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
+ tactic ctxt ("getting rid of all remaining perms",
+ full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
+ end;
fun get_derived_thm ctxt hyp concl orig_thm pi typi =
let
@@ -78,7 +78,7 @@
val _ = writeln (Syntax.string_of_term ctxt' goal_term);
in
Goal.prove ctxt' [] [] goal_term
- (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
+ (fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') |>
singleton (ProofContext.export ctxt' ctxt)
end
@@ -170,11 +170,12 @@
val get_eqvt_thms = Context.Proof #> Data.get;
val setup =
- Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
- "equivariance theorem declaration"
- #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
- "equivariance theorem declaration (without checking the form of the lemma)"
- #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get)
+ setup_nominal_eqvt_debug #>
+ Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
+ "equivariance theorem declaration" #>
+ Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
+ "equivariance theorem declaration (without checking the form of the lemma)" #>
+ PureThy.add_thms_dynamic (@{binding eqvts}, Data.get);
end;
--- a/src/HOL/Prolog/prolog.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Aug 27 18:00:45 2010 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-Unsynchronized.set Proof.show_main_goal;
+Proof.show_main_goal := true;
structure Prolog =
struct
--- a/src/HOL/String.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/String.thy Fri Aug 27 18:00:45 2010 +0200
@@ -53,7 +53,7 @@
(fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
nibbles nibbles;
in
- PureThy.note_thmss Thm.definitionK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
+ PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
#-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
end
*}
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 18:00:45 2010 +0200
@@ -679,9 +679,11 @@
end;
-val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "cooper",
- (fn (ctxt, t) => (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
- (t, procedure t)))));
+val (_, oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (@{binding cooper},
+ (fn (ctxt, t) =>
+ (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
+ (t, procedure t)))));
val comp_ss = HOL_ss addsimps @{thms semiring_norm};
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Aug 27 18:00:45 2010 +0200
@@ -310,18 +310,18 @@
(* setup *)
val setup =
- Attrib.setup (Binding.name "smt_solver")
+ Attrib.setup @{binding smt_solver}
(Scan.lift (Parse.$$$ "=" |-- Args.name) >>
(Thm.declaration_attribute o K o select_solver))
"SMT solver configuration" #>
setup_timeout #>
setup_trace #>
setup_fixed_certificates #>
- Attrib.setup (Binding.name "smt_certificates")
+ Attrib.setup @{binding smt_certificates}
(Scan.lift (Parse.$$$ "=" |-- Args.name) >>
(Thm.declaration_attribute o K o select_certificates))
"SMT certificates" #>
- Method.setup (Binding.name "smt") smt_method
+ Method.setup @{binding smt} smt_method
"Applies an SMT solver to the current goal."
--- a/src/HOL/Tools/TFL/rules.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Fri Aug 27 18:00:45 2010 +0200
@@ -46,10 +46,6 @@
val simpl_conv: simpset -> thm list -> cterm -> thm
val rbeta: thm -> thm
-(* For debugging my isabelle solver in the conditional rewriter *)
- val term_ref: term list Unsynchronized.ref
- val thm_ref: thm list Unsynchronized.ref
- val ss_ref: simpset list Unsynchronized.ref
val tracing: bool Unsynchronized.ref
val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
-> thm -> thm * term list
@@ -542,9 +538,6 @@
(*---------------------------------------------------------------------------
* Trace information for the rewriter
*---------------------------------------------------------------------------*)
-val term_ref = Unsynchronized.ref [] : term list Unsynchronized.ref
-val ss_ref = Unsynchronized.ref [] : simpset list Unsynchronized.ref;
-val thm_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref;
val tracing = Unsynchronized.ref false;
fun say s = if !tracing then writeln s else ();
@@ -665,9 +658,6 @@
val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection];
val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
- val dummy = term_ref := []
- val dummy = thm_ref := []
- val dummy = ss_ref := []
val cut_lemma' = cut_lemma RS eq_reflection
fun prover used ss thm =
let fun cong_prover ss thm =
@@ -676,8 +666,6 @@
val dummy = print_thms "cntxt:" cntxt
val dummy = say "cong rule:"
val dummy = say (Display.string_of_thm_without_context thm)
- val dummy = thm_ref := (thm :: !thm_ref)
- val dummy = ss_ref := (ss :: !ss_ref)
(* Unquantified eliminate *)
fun uq_eliminate (thm,imp,thy) =
let val tych = cterm_of thy
@@ -784,7 +772,6 @@
val dummy = tc_list := (TC :: !tc_list)
val nestedp = is_some (S.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
- val dummy = term_ref := ([func,TC]@(!term_ref))
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
else let val cTC = cterm_of thy
(HOLogic.mk_Trueprop TC)
--- a/src/HOL/Tools/meson.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Aug 27 18:00:45 2010 +0200
@@ -48,7 +48,10 @@
fun trace_msg msg = if ! trace then tracing (msg ()) else ();
val max_clauses_default = 60;
-val (max_clauses, setup) = Attrib.config_int "max_clauses" (K max_clauses_default);
+val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default);
+
+(*No known example (on 1-5-2007) needs even thirty*)
+val iter_deepen_limit = 50;
val disj_forward = @{thm disj_forward};
val disj_forward2 = @{thm disj_forward2};
@@ -640,7 +643,7 @@
end;
fun iter_deepen_prolog_tac horns =
- ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
+ ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
(fn cls =>
@@ -653,7 +656,10 @@
cat_lines ("meson method called:" ::
map (Display.string_of_thm ctxt) (cls @ ths) @
["clauses:"] @ map (Display.string_of_thm ctxt) horns))
- in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
+ in
+ THEN_ITER_DEEPEN iter_deepen_limit
+ (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
+ end));
fun meson_tac ctxt ths =
SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
--- a/src/HOL/ex/SAT_Examples.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Fri Aug 27 18:00:45 2010 +0200
@@ -10,8 +10,8 @@
(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
(* ML {* sat.solver := "minisat_with_proofs"; *} *)
-ML {* Unsynchronized.set sat.trace_sat; *}
-ML {* Unsynchronized.set quick_and_dirty; *}
+ML {* sat.trace_sat := true; *}
+ML {* quick_and_dirty := true; *}
lemma "True"
by sat
@@ -77,8 +77,8 @@
lemma "(ALL x. P x) | ~ All P"
by sat
-ML {* Unsynchronized.reset sat.trace_sat; *}
-ML {* Unsynchronized.reset quick_and_dirty; *}
+ML {* sat.trace_sat := false; *}
+ML {* quick_and_dirty := false; *}
method_setup rawsat =
{* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}
@@ -525,8 +525,8 @@
(* ML {*
sat.solver := "zchaff_with_proofs";
-Unsynchronized.reset sat.trace_sat;
-Unsynchronized.reset quick_and_dirty;
+sat.trace_sat := false;
+quick_and_dirty := false;
*} *)
ML {*
--- a/src/Pure/General/secure.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/Pure/General/secure.ML Fri Aug 27 18:00:45 2010 +0200
@@ -13,7 +13,6 @@
val use_text: use_context -> int * string -> bool -> string -> unit
val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
- val Isar_setup: unit -> unit
val PG_setup: unit -> unit
val commit: unit -> unit
val bash_output: string -> string * int
@@ -56,8 +55,8 @@
fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
-fun Isar_setup () = use_global "open Unsynchronized;";
-fun PG_setup () = use_global "structure ThyLoad = ProofGeneral.ThyLoad;";
+fun PG_setup () =
+ use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
(* shell commands *)
--- a/src/Pure/ML-Systems/unsynchronized.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/Pure/ML-Systems/unsynchronized.ML Fri Aug 27 18:00:45 2010 +0200
@@ -12,10 +12,6 @@
val op := = op :=;
val ! = !;
-fun set flag = (flag := true; true);
-fun reset flag = (flag := false; false);
-fun toggle flag = (flag := not (! flag); ! flag);
-
fun change r f = r := f (! r);
fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Aug 27 18:00:45 2010 +0200
@@ -232,7 +232,8 @@
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
| init true =
- (! initialized orelse
+ (if ! initialized then ()
+ else
(Output.no_warnings_CRITICAL init_outer_syntax ();
Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
Output.add_mode proof_generalN Output.default_output Output.default_escape;
@@ -241,8 +242,8 @@
ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
setup_thy_loader ();
setup_present_hook ();
- Unsynchronized.set initialized);
- sync_thy_loader ();
+ initialized := true);
+ sync_thy_loader ();
Unsynchronized.change print_mode (update (op =) proof_generalN);
Secure.PG_setup ();
Isar.toplevel_loop TextIO.stdIn
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Aug 27 18:00:45 2010 +0200
@@ -1021,7 +1021,8 @@
fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
| init_pgip true =
- (! initialized orelse
+ (if ! initialized then ()
+ else
(setup_preferences_tweak ();
Output.add_mode proof_generalN Output.default_output Output.default_escape;
Markup.add_mode proof_generalN YXML.output_markup;
@@ -1031,8 +1032,8 @@
setup_present_hook ();
init_pgip_session_id ();
welcome ();
- Unsynchronized.set initialized);
- sync_thy_loader ();
+ initialized := true);
+ sync_thy_loader ();
Unsynchronized.change print_mode (update (op =) proof_generalN);
pgip_toplevel tty_src);
--- a/src/Pure/System/isar.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/Pure/System/isar.ML Fri Aug 27 18:00:45 2010 +0200
@@ -134,7 +134,6 @@
fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
(Context.set_thread_data NONE;
- Secure.Isar_setup ();
if do_init then init () else ();
if welcome then writeln (Session.welcome ()) else ();
uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
--- a/src/Pure/config.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/Pure/config.ML Fri Aug 27 18:00:45 2010 +0200
@@ -41,8 +41,8 @@
| print_value (Int i) = signed_string_of_int i
| print_value (String s) = quote s;
-fun print_type (Bool _) = "boolean"
- | print_type (Int _) = "integer"
+fun print_type (Bool _) = "bool"
+ | print_type (Int _) = "int"
| print_type (String _) = "string";
fun same_type (Bool _) (Bool _) = true
--- a/src/Pure/search.ML Fri Aug 27 16:05:46 2010 +0200
+++ b/src/Pure/search.ML Fri Aug 27 18:00:45 2010 +0200
@@ -18,9 +18,8 @@
val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
val DEPTH_SOLVE: tactic -> tactic
val DEPTH_SOLVE_1: tactic -> tactic
- val iter_deepen_limit: int Unsynchronized.ref
- val THEN_ITER_DEEPEN: tactic -> (thm -> bool) -> (int -> tactic) -> tactic
- val ITER_DEEPEN: (thm -> bool) -> (int -> tactic) -> tactic
+ val THEN_ITER_DEEPEN: int -> tactic -> (thm -> bool) -> (int -> tactic) -> tactic
+ val ITER_DEEPEN: int -> (thm -> bool) -> (int -> tactic) -> tactic
val trace_DEEPEN: bool Unsynchronized.ref
val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic
val trace_BEST_FIRST: bool Unsynchronized.ref
@@ -117,21 +116,18 @@
in prune_aux (take (qs, [])) end;
-(*No known example (on 1-5-2007) needs even thirty*)
-val iter_deepen_limit = Unsynchronized.ref 50;
-
(*Depth-first iterative deepening search for a state that satisfies satp
tactic tac0 sets up the initial goal queue, while tac1 searches it.
The solution sequence is redundant: the cutoff heuristic makes it impossible
to suppress solutions arising from earlier searches, as the accumulated cost
(k) can be wrong.*)
-fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
+fun THEN_ITER_DEEPEN lim tac0 satp tac1 = traced_tac (fn st =>
let val countr = Unsynchronized.ref 0
and tf = tracify trace_DEPTH_FIRST (tac1 1)
and qs0 = tac0 st
(*bnd = depth bound; inc = estimate of increment required next*)
fun depth (bnd,inc) [] =
- if bnd > !iter_deepen_limit then
+ if bnd > lim then
(tracing (string_of_int (!countr) ^
" inferences so far. Giving up at " ^ string_of_int bnd);
NONE)
@@ -170,19 +166,19 @@
end
in depth (0,5) [] end);
-val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
+fun ITER_DEEPEN lim = THEN_ITER_DEEPEN lim all_tac;
(*Simple iterative deepening tactical. It merely "deepens" any search tactic
using increment "inc" up to limit "lim". *)
val trace_DEEPEN = Unsynchronized.ref false;
-fun DEEPEN (inc,lim) tacf m i =
+fun DEEPEN (inc, lim) tacf m i =
let
fun dpn m st =
st |>
(if has_fewer_prems i st then no_tac
- else if m>lim then
+ else if m > lim then
(if !trace_DEEPEN then tracing "Search depth limit exceeded: giving up" else ();
no_tac)
else
--- a/src/ZF/ZF.thy Fri Aug 27 16:05:46 2010 +0200
+++ b/src/ZF/ZF.thy Fri Aug 27 18:00:45 2010 +0200
@@ -10,7 +10,7 @@
uses "~~/src/Tools/misc_legacy.ML"
begin
-ML {* Unsynchronized.reset eta_contract *}
+ML {* eta_contract := false *}
typedecl i
arities i :: "term"