--- a/src/HOL/Statespace/state_space.ML Tue Oct 27 13:15:04 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Tue Oct 27 13:15:20 2009 +0100
@@ -297,7 +297,7 @@
val tt' = tt |> fold upd all_names;
val activate_simproc =
- Output.no_warnings_CRITICAL
+ Output.no_warnings_CRITICAL (* FIXME !?! *)
(Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
val ctxt' =
ctxt
--- a/src/HOL/Tools/meson.ML Tue Oct 27 13:15:04 2009 +0100
+++ b/src/HOL/Tools/meson.ML Tue Oct 27 13:15:20 2009 +0100
@@ -323,7 +323,7 @@
Strips universal quantifiers and breaks up conjunctions.
Eliminates existential quantifiers using skoths: Skolemization theorems.*)
fun cnf skoths ctxt (th,ths) =
- let val ctxtr = Unsynchronized.ref ctxt
+ let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
else if not (has_conns ["All","Ex","op &"] (prop_of th))
--- a/src/HOL/Tools/res_axioms.ML Tue Oct 27 13:15:04 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Tue Oct 27 13:15:20 2009 +0100
@@ -71,7 +71,7 @@
prefix for the Skolem constant.*)
fun declare_skofuns s th =
let
- val nref = Unsynchronized.ref 0
+ val nref = Unsynchronized.ref 0 (* FIXME ??? *)
fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
@@ -87,7 +87,8 @@
val (c, thy') =
Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
val cdef = cname ^ "_def"
- val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
+ val thy'' =
+ Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
| dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
@@ -102,7 +103,7 @@
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skofuns s th =
- let val sko_count = Unsynchronized.ref 0
+ let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
--- a/src/Pure/ML/ml_context.ML Tue Oct 27 13:15:04 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Tue Oct 27 13:15:20 2009 +0100
@@ -54,7 +54,7 @@
(* theorem bindings *)
-val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];
+val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref []; (* FIXME via context!? *)
fun ml_store sel (name, ths) =
let
@@ -195,6 +195,7 @@
fun eval_in ctxt verbose pos txt =
Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
+(* FIXME not thread-safe -- reference can be accessed directly *)
fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
let
val _ = r := NONE;
--- a/src/Pure/Thy/html.ML Tue Oct 27 13:15:04 2009 +0100
+++ b/src/Pure/Thy/html.ML Tue Oct 27 13:15:20 2009 +0100
@@ -267,7 +267,7 @@
(* document *)
val charset = Unsynchronized.ref "ISO-8859-1";
-fun with_charset s = setmp_noncritical charset s; (* FIXME *)
+fun with_charset s = setmp_noncritical charset s; (* FIXME unreliable *)
fun begin_document title =
let val cs = ! charset in
--- a/src/Pure/codegen.ML Tue Oct 27 13:15:04 2009 +0100
+++ b/src/Pure/codegen.ML Tue Oct 27 13:15:20 2009 +0100
@@ -105,7 +105,7 @@
val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
-val mode = Unsynchronized.ref ([] : string list);
+val mode = Unsynchronized.ref ([] : string list); (* FIXME proper functional argument *)
val margin = Unsynchronized.ref 80;
@@ -928,7 +928,7 @@
[str "(result ())"],
str ");"]) ^
"\n\nend;\n";
- val _ = NAMED_CRITICAL "codegen" (fn () =>
+ val _ = NAMED_CRITICAL "codegen" (fn () => (* FIXME ??? *)
ML_Context.eval_in (SOME ctxt) false Position.none s);
in !eval_result end;
in e () end;