# HG changeset patch
# User wenzelm
# Date 1256645720 -3600
# Node ID 89ced80833ac90e8a9acdc6f053df76cf50fadce
# Parent  5bb809208876ba827d172a1eab740030f15c9dd4
critical comments;

diff -r 5bb809208876 -r 89ced80833ac src/HOL/Statespace/state_space.ML
--- 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
diff -r 5bb809208876 -r 89ced80833ac src/HOL/Tools/meson.ML
--- 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))
diff -r 5bb809208876 -r 89ced80833ac src/HOL/Tools/res_axioms.ML
--- 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*)
diff -r 5bb809208876 -r 89ced80833ac src/Pure/ML/ml_context.ML
--- 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;
diff -r 5bb809208876 -r 89ced80833ac src/Pure/Thy/html.ML
--- 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
diff -r 5bb809208876 -r 89ced80833ac src/Pure/codegen.ML
--- 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;