eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
modernized attribute setup;

--- a/src/HOL/Statespace/state_space.ML	Fri Aug 27 21:16:11 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Aug 27 21:22:07 2010 +0200
@@ -277,28 +277,29 @@
     fun comps_of_thm thm = prop_of thm
              |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free);
 
-    fun type_attr phi (ctxt,thm) =
-      (case ctxt of Context.Theory _ => (ctxt,thm)
-       | _ =>
+    fun type_attr phi = Thm.declaration_attribute (fn thm => fn context =>
+      (case context of
+        Context.Theory _ => context
+      | Context.Proof ctxt =>
         let
-          val {declinfo,distinctthm=tt,silent} = (NameSpaceData.get ctxt);
+          val {declinfo,distinctthm=tt,silent} = NameSpaceData.get context;
           val all_names = comps_of_thm thm;
           fun upd name tt =
-               (case (Symtab.lookup tt name) of
+               (case Symtab.lookup tt name of
                  SOME dthm => if sorted_subset (op =) (comps_of_thm dthm) all_names
                               then Symtab.update (name,thm) tt else tt
-                | NONE => Symtab.update (name,thm) tt)
+               | NONE => Symtab.update (name,thm) tt)
 
           val tt' = tt |> fold upd all_names;
           val activate_simproc =
-              Output.no_warnings_CRITICAL   (* FIXME !?! *)
-               (Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
-          val ctxt' =
-              ctxt
+            Simplifier.map_ss
+              (Simplifier.with_context (Context_Position.set_visible false ctxt)
+                (fn ss => ss addsimprocs [distinct_simproc]));
+          val context' =
+              context
               |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent}
-              |> activate_simproc
-        in (ctxt',thm)
-        end)
+              |> activate_simproc;
+        in context' end));
 
     val attr = Attrib.internal type_attr;