eliminated quiete_mode ref (not really needed);

--- a/src/HOL/Statespace/state_space.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -14,8 +14,6 @@
     val projectN : string
     val valuetypesN : string
 
-    val quiet_mode : bool ref
-
     val namespace_definition :
        bstring ->
        Term.typ ->
@@ -35,7 +33,7 @@
        (string * Term.typ) list -> Context.theory -> Context.theory
 
     val statespace_decl :
-       OuterParse.token list -> 
+       OuterParse.token list ->
        ((string list * bstring) *
          ((string list * xstring * (bstring * bstring) list) list *
           (bstring * string) list)) * OuterParse.token list
@@ -89,20 +87,15 @@
 val KN = "StateFun.K_statefun"
 
 
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
 (* Library *)
 
 fun fold1 f xs = fold f (tl xs) (hd xs)
 fun fold1' f [] x = x
   | fold1' f xs _ = fold1 f xs
- 
-fun sublist_idx eq xs ys = 
+
+fun sublist_idx eq xs ys =
   let
-    fun sublist n xs ys = 
+    fun sublist n xs ys =
          if is_prefix eq xs ys then SOME n
          else (case ys of [] => NONE
                | (y::ys') => sublist (n+1) xs ys')
@@ -122,10 +115,10 @@
   distinctthm: thm Symtab.table,
   silent: bool
  };
- 
+
 structure NameSpaceArgs =
 struct
-  type T = namespace_info; 
+  type T = namespace_info;
   val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false};
   val extend = I;
   fun merge pp ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
@@ -143,29 +136,29 @@
 
 fun delete_declinfo n ctxt =
   let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
-  in NameSpaceData.put 
+  in NameSpaceData.put
        (make_namespace_data (Termtab.delete_safe n declinfo) distinctthm silent) ctxt
   end;
 
 
 fun update_declinfo (n,v) ctxt =
   let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
-  in NameSpaceData.put 
+  in NameSpaceData.put
       (make_namespace_data (Termtab.update (n,v) declinfo) distinctthm silent) ctxt
   end;
 
 fun set_silent silent ctxt =
   let val {declinfo,distinctthm,...} = NameSpaceData.get ctxt;
-  in NameSpaceData.put 
+  in NameSpaceData.put
       (make_namespace_data declinfo distinctthm silent) ctxt
   end;
 
 val get_silent = #silent o NameSpaceData.get;
- 
+
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
    |> Locale.interpretation_in_locale I (name, expr)
-   |> Proof.global_terminal_proof 
+   |> Proof.global_terminal_proof
          (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
    |> ProofContext.theory_of
 
@@ -190,32 +183,32 @@
 structure StateSpaceData = GenericDataFun(StateSpaceArgs);
 
 fun add_statespace name args parents components types ctxt =
-     StateSpaceData.put 
+     StateSpaceData.put
       (Symtab.update_new (name, {args=args,parents=parents,
                                 components=components,types=types}) (StateSpaceData.get ctxt))
-      ctxt; 
+      ctxt;
 
 fun get_statespace ctxt name =
       Symtab.lookup (StateSpaceData.get ctxt) name;
 
 
-fun lookupI eq xs n = 
+fun lookupI eq xs n =
   (case AList.lookup eq xs n of
      SOME v => v
    | NONE => n);
- 
+
 fun mk_free ctxt name =
-  if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name 
+  if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
   then
     let val n' = lookupI (op =) (Variable.fixes_of ctxt) name
     in SOME (Free (n',ProofContext.infer_type ctxt n')) end
   else NONE
-  
-     
+
+
 fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name;
-fun get_comp ctxt name = 
-     Option.mapPartial 
-       (Termtab.lookup (#declinfo (NameSpaceData.get ctxt))) 
+fun get_comp ctxt name =
+     Option.mapPartial
+       (Termtab.lookup (#declinfo (NameSpaceData.get ctxt)))
        (mk_free (Context.proof_of ctxt) name);
 
 
@@ -223,17 +216,17 @@
 
 fun neq_x_y ctxt x y =
   (let
-    val dist_thm = the (get_dist_thm (Context.Proof ctxt) (#1 (dest_Free x))); 
+    val dist_thm = the (get_dist_thm (Context.Proof ctxt) (#1 (dest_Free x)));
     val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
     val tree = term_of ctree;
     val x_path = the (DistinctTreeProver.find_tree x tree);
     val y_path = the (DistinctTreeProver.find_tree y tree);
     val thm = DistinctTreeProver.distinctTreeProver dist_thm x_path y_path;
-  in SOME thm  
+  in SOME thm
   end handle Option => NONE)
 
-fun distinctTree_tac ctxt 
-      (Const ("Trueprop",_) $ 
+fun distinctTree_tac ctxt
+      (Const ("Trueprop",_) $
         (Const ("Not", _) $ (Const ("op =", _) $ (x as Free _)$ (y as Free _))), i) =
   (case (neq_x_y ctxt x y) of
      SOME neq => rtac neq i
@@ -249,13 +242,13 @@
   Simplifier.simproc HOL.thy "StateSpace.distinct_simproc" ["x = y"]
     (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
         (case #context (#1 (rep_ss ss)) of
-          SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) 
-                       (neq_x_y ctxt x y) 
+          SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
+                       (neq_x_y ctxt x y)
         | NONE => NONE)
       | _ => NONE))
 
-fun change_simpset f = 
-     Context.mapping 
+fun change_simpset f =
+     Context.mapping
        (fn thy  => (change_simpset_of thy f; thy))
        (fn ctxt => Simplifier.put_local_simpset (f (Simplifier.get_local_simpset ctxt)) ctxt);
 
@@ -263,9 +256,9 @@
   Sign.read_typ thy s;
 
 local
-  val ss = HOL_basic_ss 
-in    
-fun interprete_parent name dist_thm_name parent_expr thy = 
+  val ss = HOL_basic_ss
+in
+fun interprete_parent name dist_thm_name parent_expr thy =
   let
 
     fun solve_tac ctxt (_,i) st =
@@ -275,20 +268,20 @@
         val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
       in EVERY [rtac rule i] st
       end
-        
+
     fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [],
-                          ALLGOALS (SUBGOAL (solve_tac ctxt))] 
-        
-  in thy 
+                          ALLGOALS (SUBGOAL (solve_tac ctxt))]
+
+  in thy
      |> prove_interpretation_in tac (name,parent_expr)
-  end;        
+  end;
 
 end;
 
-fun namespace_definition name nameT parent_expr parent_comps new_comps thy = 
+fun namespace_definition name nameT parent_expr parent_comps new_comps thy =
   let
     val all_comps = parent_comps @ new_comps;
-    val vars = Locale.Merge 
+    val vars = Locale.Merge
                 (map (fn n => Locale.Rename (Locale.Locale (Locale.intern thy "var")
                                             ,[SOME (n,NONE)])) all_comps);
 
@@ -298,13 +291,13 @@
         let val prefix = fold1' (fn name => fn prfx => prfx ^ "_" ^ name) all_comps "";
         in if prefix = "" then dist_thm_name else prefix ^ "." ^ dist_thm_name end;
 
-    fun comps_of_thm thm = prop_of thm 
+    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)
        | _ =>
-        let 
+        let
           val {declinfo,distinctthm=tt,silent} = (NameSpaceData.get ctxt);
 	  val all_names = comps_of_thm thm;
           fun upd name tt =
@@ -315,28 +308,28 @@
 
           val tt' = tt |> fold upd all_names;
           val activate_simproc =
-              Output.no_warnings 
+              Output.no_warnings
                (change_simpset (fn ss => ss addsimprocs [distinct_simproc]));
           val ctxt' =
-              ctxt 
+              ctxt
               |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent}
               |> activate_simproc
-        in (ctxt',thm) 
+        in (ctxt',thm)
         end)
-        
+
     val attr = Attrib.internal type_attr;
 
-    val assumes = Element.Assumes [((dist_thm_name,[attr]), 
+    val assumes = Element.Assumes [((dist_thm_name,[attr]),
                     [(HOLogic.Trueprop $
                       (Const ("DistinctTreeProver.all_distinct",
                                  Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $
-                      DistinctTreeProver.mk_tree (fn n => Free (n,nameT)) nameT 
+                      DistinctTreeProver.mk_tree (fn n => Free (n,nameT)) nameT
                                 (sort fast_string_ord all_comps)),
                       ([]))])];
 
-  in thy 
+  in thy
      |> Locale.add_locale_i (SOME "") name vars [assumes]
-     ||> ProofContext.theory_of 
+     ||> ProofContext.theory_of
      ||> interprete_parent name dist_thm_full_name parent_expr
      |> #2
   end;
@@ -347,7 +340,7 @@
 
 fun encode_type (TFree (s, _)) = s
   | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
-  | encode_type (Type (n,Ts)) = 
+  | encode_type (Type (n,Ts)) =
       let
         val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) "";
         val n' = String.map encode_dot n;
@@ -365,7 +358,7 @@
 fun put_const n T nT V = Free (put_name n, T --> (nT --> V) --> (nT --> V));
 
 fun lookup_const T nT V = Const ("StateFun.lookup",(V --> T) --> nT --> (nT --> V) --> T);
-fun update_const T nT V = 
+fun update_const T nT V =
  Const ("StateFun.update",
           (V --> T) --> (T --> V) --> nT --> (T --> T) --> (nT --> V) --> (nT --> V));
 
@@ -378,7 +371,7 @@
   thy
   |> TheoryTarget.init name
   |> (fn lthy => LocalTheory.declaration (decl lthy) lthy)
-  |> LocalTheory.exit 
+  |> LocalTheory.exit
   |> ProofContext.theory_of;
 
 fun parent_components thy (Ts, pname, renaming) =
@@ -387,11 +380,11 @@
     fun rename [] xs = xs
       | rename (NONE::rs)  (x::xs) = x::rename rs xs
       | rename (SOME r::rs) ((x,T)::xs) = (r,T)::rename rs xs;
-    val {args,parents,components,...} = 
+    val {args,parents,components,...} =
 	      the (Symtab.lookup (StateSpaceData.get ctxt) pname);
     val inst = map fst args ~~ Ts;
     val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
-    val parent_comps = 
+    val parent_comps =
      List.concat (map (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents);
     val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
   in all_comps end;
@@ -399,13 +392,13 @@
 fun take_upto i xs = List.take(xs,i) handle Subscript => xs;
 
 fun statespace_definition state_type args name parents parent_comps components thy =
-  let 
+  let
     val full_name = Sign.full_name thy name;
     val all_comps = parent_comps @ components;
 
     val components' = map (fn (n,T) => (n,(T,full_name))) components;
-    val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps; 
-    fun parent_expr (_,n,rs) = Locale.Rename 
+    val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
+    fun parent_expr (_,n,rs) = Locale.Rename
                                 (Locale.Locale (suffix namespaceN n),
                                  map (Option.map (fn s => (s,NONE))) rs);
     val parents_expr = Locale.Merge (fold (fn p => fn es => parent_expr p::es) parents []);
@@ -422,73 +415,73 @@
     val nameT = TFree (nameN, Sign.defaultS thy);
     val stateT = nameT --> valueT;
     fun projectT T = valueT --> T;
-    fun injectT T = T --> valueT; 
+    fun injectT T = T --> valueT;
 
     val locs = map (fn T => Locale.Rename (Locale.Locale project_injectL,
                              [SOME (project_name T,NONE),
                               SOME (inject_name T ,NONE)])) Ts;
-    val constrains = List.concat 
+    val constrains = List.concat
          (map (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts);
 
-    fun interprete_parent_valuetypes (Ts, pname, _) = 
+    fun interprete_parent_valuetypes (Ts, pname, _) =
       let
-        val {args,types,...} = 
+        val {args,types,...} =
              the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
         val inst = map fst args ~~ Ts;
         val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
         val pars = List.concat (map ((fn T => [project_name T,inject_name T]) o subst) types);
         val expr = Locale.Rename (Locale.Locale (suffix valuetypesN name),
                                   map (fn n => SOME (n,NONE)) pars);
-      in prove_interpretation_in (K all_tac) 
+      in prove_interpretation_in (K all_tac)
            (suffix valuetypesN name, expr) end;
 
     fun interprete_parent (_, pname, rs) =
       let
         val expr = Locale.Rename (Locale.Locale pname, map (Option.map (fn n => (n,NONE))) rs)
-      in prove_interpretation_in 
-           (fn ctxt => Locale.intro_locales_tac false ctxt []) 
+      in prove_interpretation_in
+           (fn ctxt => Locale.intro_locales_tac false ctxt [])
            (full_name, expr) end;
 
     fun declare_declinfo updates lthy phi ctxt =
       let
-        fun upd_prf ctxt = 
+        fun upd_prf ctxt =
           let
             fun upd (n,v) =
               let
                 val nT = ProofContext.infer_type (LocalTheory.target_of lthy) n
-              in Context.proof_map 
-                  (update_declinfo (Morphism.term phi (Free (n,nT)),v))  
+              in Context.proof_map
+                  (update_declinfo (Morphism.term phi (Free (n,nT)),v))
               end;
           in ctxt |> fold upd updates end;
 
       in Context.mapping I upd_prf ctxt end;
 
-   fun string_of_typ T = 
-      setmp show_sorts true 
+   fun string_of_typ T =
+      setmp show_sorts true
        (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
    val fixestate = (case state_type of
          NONE => []
-       | SOME s => 
-          let 
+       | SOME s =>
+          let
 	    val fx = Element.Fixes [(s,SOME (string_of_typ stateT),NoSyn)];
-            val cs = Element.Constrains 
+            val cs = Element.Constrains
                        (map (fn (n,T) =>  (n,string_of_typ T))
                          ((map (fn (n,_) => (n,nameT)) all_comps) @
                           constrains))
           in [fx,cs] end
        )
 
-   
-  in thy 
-     |> namespace_definition 
-           (suffix namespaceN name) nameT parents_expr 
+
+  in thy
+     |> namespace_definition
+           (suffix namespaceN name) nameT parents_expr
            (map fst parent_comps) (map fst components)
      |> Context.theory_map (add_statespace full_name args parents components [])
-     |> Locale.add_locale_i (SOME "") (suffix valuetypesN name) (Locale.Merge locs) 
+     |> Locale.add_locale_i (SOME "") (suffix valuetypesN name) (Locale.Merge locs)
             [Element.Constrains constrains]
      |> ProofContext.theory_of o #2
-     |> fold interprete_parent_valuetypes parents 
-     |> Locale.add_locale (SOME "") name 
+     |> fold interprete_parent_valuetypes parents
+     |> Locale.add_locale (SOME "") name
               (Locale.Merge [Locale.Locale (suffix namespaceN full_name)
                             ,Locale.Locale (suffix valuetypesN full_name)]) fixestate
      |> ProofContext.theory_of o #2
@@ -521,30 +514,30 @@
 fun gen_define_statespace prep_typ state_space args name parents comps thy =
   let (* - args distinct
          - only args may occur in comps and parent-instantiations
-         - number of insts must match parent args 
+         - number of insts must match parent args
          - no duplicate renamings
          - renaming should occur in namespace
       *)
-    val _ = message ("Defining statespace " ^ quote name ^ " ...");
+    val _ = writeln ("Defining statespace " ^ quote name ^ " ...");
 
     fun add_parent (Ts,pname,rs) env =
       let
         val full_pname = Sign.full_name thy pname;
-        val {args,components,...} = 
+        val {args,components,...} =
               (case get_statespace (Context.Theory thy) full_pname of
                 SOME r => r
                | NONE => error ("Undefined statespace " ^ quote pname));
 
 
         val (Ts',env') = fold_map (prep_typ thy) Ts env
-            handle ERROR msg => cat_error msg 
-                    ("The error(s) above occured in parent statespace specification " 
+            handle ERROR msg => cat_error msg
+                    ("The error(s) above occured in parent statespace specification "
                     ^ quote pname);
         val err_insts = if length args <> length Ts' then
             ["number of type instantiation(s) does not match arguments of parent statespace "
               ^ quote pname]
             else [];
-        
+
         val rnames = map fst rs
         val err_dup_renamings = (case duplicates (op =) rnames of
              [] => []
@@ -554,23 +547,23 @@
         val err_rename_unknowns = (case (filter (fn n => not (n mem cnames))) rnames of
               [] => []
              | rs => ["Unknown components " ^ commas rs]);
-              
+
 
         val rs' = map (AList.lookup (op =) rs o fst) components;
         val errs =err_insts @ err_dup_renamings @ err_rename_unknowns
       in if null errs then ((Ts',full_pname,rs'),env')
          else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
       end;
- 
+
     val (parents',env) = fold_map add_parent parents [];
 
     val err_dup_args =
          (case duplicates (op =) args of
             [] => []
           | dups => ["Duplicate type argument(s) " ^ commas dups]);
-    
+
 
-    val err_dup_components = 
+    val err_dup_components =
          (case duplicates (op =) (map fst comps) of
            [] => []
           | dups => ["Duplicate state-space components " ^ commas dups]);
@@ -592,16 +585,16 @@
 
 
     fun fst_eq ((x:string,_),(y,_)) = x = y;
-    fun snd_eq ((_,t:typ),(_,u)) = t = u;              
+    fun snd_eq ((_,t:typ),(_,u)) = t = u;
 
     val raw_parent_comps = (List.concat (map (parent_components thy) parents'));
-    fun check_type (n,T) = 
+    fun check_type (n,T) =
           (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
              []  => []
            | [_] => []
-           | rs  => ["Different types for component " ^ n ^": " ^ commas 
+           | rs  => ["Different types for component " ^ n ^": " ^ commas
                        (map (Pretty.string_of o Display.pretty_ctyp o ctyp_of thy o snd) rs)])
-                           
+
     val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps))
 
     val parent_comps = distinct (fst_eq) raw_parent_comps;
@@ -612,24 +605,24 @@
     val errs = err_dup_args @ err_dup_components @ err_extra_frees @
                err_dup_types @ err_comp_in_parent;
 
-  in if null errs 
+  in if null errs
      then thy |> statespace_definition state_space args' name parents' parent_comps comps'
-     else error (cat_lines errs) 
+     else error (cat_lines errs)
   end
   handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name);
- 
+
 
 val define_statespace = gen_define_statespace read_typ NONE;
 val define_statespace_i = gen_define_statespace cert_typ;
- 
+
 
 (*** parse/print - translations ***)
 
 
 local
-fun map_get_comp f ctxt (Free (name,_)) = 
-      (case (get_comp ctxt name) of 
-        SOME (T,_) => f T T dummyT 
+fun map_get_comp f ctxt (Free (name,_)) =
+      (case (get_comp ctxt name) of
+        SOME (T,_) => f T T dummyT
       | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*)))
   | map_get_comp _ _ _ = Syntax.free "arbitrary";
 
@@ -639,11 +632,11 @@
 fun name_of (Free (n,_)) = n;
 in
 
-fun gen_lookup_tr ctxt s n = 
+fun gen_lookup_tr ctxt s n =
       (case get_comp (Context.Proof ctxt) n of
-        SOME (T,_) => 
+        SOME (T,_) =>
            Syntax.const "StateFun.lookup"$Syntax.free (project_name T)$Syntax.free n$s
-       | NONE => 
+       | NONE =>
            if get_silent (Context.Proof ctxt)
 	   then Syntax.const "StateFun.lookup"$Syntax.const "arbitrary"$Syntax.free n$s
            else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
@@ -654,12 +647,12 @@
 fun lookup_tr' ctxt [_$Free (prj,_),n as (_$Free (name,_)),s] =
      ( case get_comp (Context.Proof ctxt) name of
          SOME (T,_) =>  if prj=project_name T then
-                           Syntax.const "_statespace_lookup" $ s $ n  
+                           Syntax.const "_statespace_lookup" $ s $ n
                         else raise Match
       | NONE => raise Match)
   | lookup_tr' _ ts = raise Match;
 
-fun gen_update_tr id ctxt n v s = 
+fun gen_update_tr id ctxt n v s =
   let
     fun pname T = if id then "Fun.id" else project_name T
     fun iname T = if id then "Fun.id" else inject_name T
@@ -668,8 +661,8 @@
        SOME (T,_) => Syntax.const "StateFun.update"$
                    Syntax.free (pname T)$Syntax.free (iname T)$
                    Syntax.free n$(Syntax.const KN $ v)$s
-      | NONE => 
-         if get_silent (Context.Proof ctxt) 
+      | NONE =>
+         if get_silent (Context.Proof ctxt)
          then Syntax.const "StateFun.update"$
                    Syntax.const "arbitrary"$Syntax.const "arbitrary"$
                    Syntax.free n$(Syntax.const KN $ v)$s
@@ -682,7 +675,7 @@
      if NameSpace.base k = NameSpace.base KN then
         (case get_comp (Context.Proof ctxt) name of
           SOME (T,_) => if inj=inject_name T andalso prj=project_name T then
-                           Syntax.const "_statespace_update" $ s $ n $ v  
+                           Syntax.const "_statespace_update" $ s $ n $ v
                         else raise Match
          | NONE => raise Match)
      else raise Match
@@ -697,7 +690,7 @@
 
 val type_insts =
   P.typ >> single ||
-  P.$$$ "(" |-- P.!!! (P.list1 P.typ --| P.$$$ ")") 
+  P.$$$ "(" |-- P.!!! (P.list1 P.typ --| P.$$$ ")")
 
 val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ);
 fun plus1_unless test scan =
@@ -714,14 +707,14 @@
 
 val statespace_decl =
    P.type_args -- P.name --
-    (P.$$$ "=" |-- 
+    (P.$$$ "=" |--
      ((Scan.repeat1 comp >> pair []) ||
       (plus1_unless comp parent --
         Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 comp)) [])))
 
 val statespace_command =
   OuterSyntax.command "statespace" "define state space" K.thy_decl
-  (statespace_decl >> (fn ((args,name),(parents,comps)) => 
+  (statespace_decl >> (fn ((args,name),(parents,comps)) =>
                            Toplevel.theory (define_statespace args name parents comps)))
 
 end;

--- a/src/HOL/Tools/TFL/post.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -8,9 +8,6 @@
 
 signature TFL =
 sig
-  val trace: bool ref
-  val quiet_mode: bool ref
-  val message: string -> unit
   val tgoalw: theory -> thm list -> thm list -> thm list
   val tgoal: theory -> thm list -> thm list
   val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
@@ -26,15 +23,6 @@
 
 structure S = USyntax
 
-
-(* messages *)
-
-val trace = Prim.trace
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
 (* misc *)
 
 (*---------------------------------------------------------------------------
@@ -120,15 +108,15 @@
 in
 fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
   let
-    val _ = message "Proving induction theorem ..."
+    val _ = writeln "Proving induction theorem ..."
     val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
-    val _ = message "Postprocessing ...";
+    val _ = writeln "Postprocessing ...";
     val {rules, induction, nested_tcs} =
       std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
   in
   case nested_tcs
   of [] => {induction=induction, rules=rules,tcs=[]}
-  | L  => let val dummy = message "Simplifying nested TCs ..."
+  | L  => let val dummy = writeln "Simplifying nested TCs ..."
               val (solved,simplified,stubborn) =
                fold_rev (fn th => fn (So,Si,St) =>
                      if (id_thm th) then (So, Si, th::St) else
@@ -144,7 +132,7 @@
               val dummy = Prim.trace_thms "Simplifying the recursion rules..."
                                           [rules]
               val rules'     = rewr rules
-              val _ = message "... Postprocessing finished";
+              val _ = writeln "... Postprocessing finished";
           in
           {induction = induction',
                rules = rules',
@@ -263,7 +251,7 @@
  let val {rules,R,theory,full_pats_TCs,SV,...} =
              Prim.lazyR_def thy (Sign.base_name fid) congs eqs
      val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
-     val dummy = message "Proving induction theorem ...";
+     val dummy = writeln "Proving induction theorem ...";
      val induction = Prim.mk_induction theory
                         {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
  in (theory,

--- a/src/HOL/Tools/old_primrec_package.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -7,7 +7,6 @@
 
 signature OLD_PRIMREC_PACKAGE =
 sig
-  val quiet_mode: bool ref
   val unify_consts: theory -> term list -> term list -> term list * term list
   val add_primrec: string -> ((bstring * string) * Attrib.src list) list
     -> theory -> thm list * theory
@@ -31,12 +30,6 @@
   primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
 
 
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
 (*the following code ensures that each recursive set always has the
   same type in all introduction rules*)
 fun unify_consts thy cs intr_ts =
@@ -283,8 +276,6 @@
       |> Sign.add_path primrec_name
       |> fold_map def (map (fn (name, t) => ((name, []), t)) defs');
     val rewrites = (map mk_meta_eq rec_rewrites) @ map snd defs_thms';
-    val _ = message ("Proving equations for primrec function(s) " ^
-      commas_quote (map fst nameTs1) ^ " ...");
     val simps = map (fn (_, t) => Goal.prove_global thy' [] [] t
         (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
     val (simps', thy'') =

--- a/src/HOL/Tools/recdef_package.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -7,7 +7,6 @@
 
 signature RECDEF_PACKAGE =
 sig
-  val quiet_mode: bool ref
   val get_recdef: theory -> string
     -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
   val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
@@ -34,9 +33,6 @@
 structure RecdefPackage: RECDEF_PACKAGE =
 struct
 
-val quiet_mode = Tfl.quiet_mode;
-val message = Tfl.message;
-
 
 (** recdef hints **)
 
@@ -198,7 +194,7 @@
 
     val name = Sign.intern_const thy raw_name;
     val bname = Sign.base_name name;
-    val _ = message ("Defining recursive function " ^ quote name ^ " ...");
+    val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
 
     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
@@ -239,7 +235,7 @@
     val bname = Sign.base_name name;
 
     val _ = requires_recdef thy;
-    val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
+    val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
 
     val (congs, thy1) = thy |> app_thms raw_congs;
     val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;

--- a/src/HOL/Tools/specification_package.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/HOL/Tools/specification_package.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -7,7 +7,6 @@
 
 signature SPECIFICATION_PACKAGE =
 sig
-  val quiet_mode: bool ref
   val add_specification: string option -> (bstring * xstring * bool) list ->
     theory * thm -> theory * thm
 end
@@ -15,17 +14,9 @@
 structure SpecificationPackage: SPECIFICATION_PACKAGE =
 struct
 
-(* messages *)
-
-val quiet_mode = ref false
-fun message s = if ! quiet_mode then () else writeln s
-
-
-(* Actual code *)
+(* actual code *)
 
 local
-    val exE_some = thm "exE_some";
-
     fun mk_definitional [] arg = arg
       | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
         case HOLogic.dest_Trueprop (concl_of thm) of
@@ -39,7 +30,7 @@
                 val def_eq = Logic.mk_equals (Const(cname_full,ctype),
                                               HOLogic.choice_const ctype $  P)
                 val (thms, thy') = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
-                val thm' = [thm,hd thms] MRS exE_some
+                val thm' = [thm,hd thms] MRS @{thm exE_some}
             in
                 mk_definitional cos (thy',thm')
             end

--- a/src/HOL/Tools/typedef_package.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -8,7 +8,6 @@
 
 signature TYPEDEF_PACKAGE =
 sig
-  val quiet_mode: bool ref
   type info =
    {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
     type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
@@ -48,12 +47,6 @@
 
 (** type definitions **)
 
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
 (* theory data *)
 
 type info =
@@ -227,17 +220,12 @@
 
 fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
   let
-    val string_of_term = Sign.string_of_term thy;
     val name = the_default (#1 typ) opt_name;
     val (set, goal, _, typedef_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
-    val _ = message ("Proving non-emptiness of set " ^ quote (string_of_term set) ^ " ...");
     val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
-      cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_term set));
-  in
-    thy
-    |> typedef_result non_empty
-  end;
+      cat_error msg ("Failed to prove non-emptiness of " ^ quote (Sign.string_of_term thy set));
+  in typedef_result non_empty thy end;
 
 in
 

--- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -8,7 +8,6 @@
 
 signature PCPODEF_PACKAGE =
 sig
-  val quiet_mode: bool ref
   val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
     * (string * string) option -> theory -> Proof.state
   val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
@@ -42,12 +41,6 @@
 
 (** type definitions **)
 
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
 (* prepare_cpodef *)
 
 fun err_in_cpodef msg name =

--- a/src/ZF/Tools/primrec_package.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -9,7 +9,6 @@
 
 signature PRIMREC_PACKAGE =
 sig
-  val quiet_mode: bool ref
   val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
   val add_primrec_i: ((bstring * term) * attribute list) list -> theory -> theory * thm list
 end;
@@ -17,12 +16,6 @@
 structure PrimrecPackage : PRIMREC_PACKAGE =
 struct
 
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
 exception RecError of string;
 
 (*Remove outer Trueprop and equality sign*)
@@ -181,10 +174,9 @@
 
     val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
     val eqn_thms =
-     (message ("Proving equations for primrec function " ^ fname);
       eqn_terms |> map (fn t =>
         Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
-          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])));
+          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]));
 
     val (eqn_thms', thy2) =
       thy1