removed conditional combinator;

--- a/src/HOL/Tools/record_package.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -475,6 +475,7 @@
 
 val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get;
 
+
 (* parent records *)
 
 fun add_parents thy NONE parents = parents
@@ -490,6 +491,7 @@
         fun bad_inst ((x, S), T) =
           if Sign.of_sort sign (T, S) then NONE else SOME x
         val bads = List.mapPartial bad_inst (args ~~ types);
+        val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
 
         val inst = map fst args ~~ types;
         val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
@@ -497,13 +499,12 @@
         val fields' = map (apsnd subst) fields;
         val extension' = apsnd (map subst) extension;
       in
-        conditional (not (null bads)) (fn () =>
-          err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
         add_parents thy parent'
-          (make_parent_info name fields' extension' induct::parents)
+          (make_parent_info name fields' extension' induct :: parents)
       end;
 
 
+
 (** concrete syntax for records **)
 
 (* parse translations *)

--- a/src/HOL/ex/svc_funcs.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/HOL/ex/svc_funcs.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -243,8 +243,7 @@
 
  (*The oracle proves the given formula t, if possible*)
  fun oracle thy t =
-  (conditional (! trace) (fn () =>
-    tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t));
-  if valid (expr_of false t) then t else fail t);
+  (if ! trace then tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t) else ();
+   if valid (expr_of false t) then t else fail t);
 
 end;

--- a/src/Pure/General/file.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/General/file.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -137,12 +137,15 @@
     SOME ids => OS.FileSys.compare ids = EQUAL
   | NONE => false);
 
-fun copy src dst = conditional (not (eq (src, dst))) (fn () =>
-  let val target = if is_dir dst then Path.append dst (Path.base src) else dst
-  in write target (read src) end);
+fun copy src dst =
+  if eq (src, dst) then ()
+  else
+    let val target = if is_dir dst then Path.append dst (Path.base src) else dst
+    in write target (read src) end;
 
-fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
-  (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
+fun copy_dir src dst =
+  if eq (src, dst) then ()
+  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
 
 
 (* use ML files *)

--- a/src/Pure/General/name_space.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/General/name_space.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -232,11 +232,11 @@
   if is_hidden name then
     error ("Attempt to declare hidden name " ^ quote name)
   else
-    let val names = explode_name name in
-      conditional (null names orelse exists (fn s => s = "") names) (fn () =>
-        error ("Bad name declaration " ^ quote name));
-      fold (add_name name) (map implode_name (accs names)) space
-    end;
+    let
+      val names = explode_name name;
+      val _ = (null names orelse exists (fn s => s = "") names) andalso
+        error ("Bad name declaration " ^ quote name);
+    in fold (add_name name) (map implode_name (accs names)) space end;
 
 
 (* manipulate namings *)

--- a/src/Pure/Isar/locale.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -1070,10 +1070,10 @@
     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
     fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
   in
-    conditional (exists (equal y o #1) xs) (fn () =>
-      err "Attempt to define previously specified variable");
-    conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
-      err "Attempt to redefine variable");
+    exists (equal y o #1) xs andalso
+      err "Attempt to define previously specified variable";
+    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
+      err "Attempt to redefine variable";
     (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
   end;
 
@@ -1763,8 +1763,8 @@
     do_predicate bname raw_import raw_body thy =
   let
     val name = Sign.full_name thy bname;
-    val _ = conditional (is_some (get_locale thy name)) (fn () =>
-      error ("Duplicate definition of locale " ^ quote name));
+    val _ = is_some (get_locale thy name) andalso
+      error ("Duplicate definition of locale " ^ quote name);
 
     val thy_ctxt = ProofContext.init thy;
     val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),

--- a/src/Pure/Isar/method.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/Isar/method.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -246,9 +246,10 @@
 val trace_rules = ref false;
 
 fun trace ctxt rules =
-  conditional (! trace_rules andalso not (null rules)) (fn () =>
+  if ! trace_rules andalso not (null rules) then
     Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
-    |> Pretty.string_of |> tracing);
+    |> Pretty.string_of |> tracing
+  else ();
 
 local
 

--- a/src/Pure/Isar/toplevel.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -661,8 +661,9 @@
 
 fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
   let
-    val _ = conditional (not int andalso int_only) (fn () =>
-      warning (command_msg "Interactive-only " tr));
+    val _ =
+      if not int andalso int_only then warning (command_msg "Interactive-only " tr)
+      else ();
 
     fun do_timing f x = (Output.info (command_msg "" tr); timeap f x);
     fun do_profiling f x = profile (! profiling) f x;
@@ -671,9 +672,9 @@
        state |> (apply_trans int trans
         |> (if ! profiling > 0 then do_profiling else I)
         |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
-    val _ = conditional (int andalso not (! quiet) andalso
-        exists (member (op =) print) ("" :: ! print_mode))
-      (fn () => print_state false result);
+    val _ =
+      if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: ! print_mode)
+      then print_state false result else ();
   in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
 
 in

--- a/src/Pure/Syntax/ast.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/Syntax/ast.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -205,8 +205,9 @@
       | rewrite ast = try_headless_rules ast;
 
     fun rewrote old_ast new_ast =
-      conditional trace (fn () =>
-        tracing ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast));
+      if trace then
+        tracing ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
+      else ();
 
     fun norm_root ast =
       (case rewrite ast of
@@ -234,17 +235,16 @@
       end;
 
 
-    val _ = conditional trace (fn () => tracing ("pre: " ^ str_of_ast pre_ast));
-
+    val _ = if trace then tracing ("pre: " ^ str_of_ast pre_ast) else ();
     val post_ast = normal pre_ast;
-  in
-    conditional (trace orelse stat) (fn () =>
-      tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
-        string_of_int (! passes) ^ " passes, " ^
-        string_of_int (! changes) ^ " changes, " ^
-        string_of_int (! failed_matches) ^ " matches failed"));
-    post_ast
-  end;
+    val _ =
+      if trace orelse stat then
+        tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
+          string_of_int (! passes) ^ " passes, " ^
+          string_of_int (! changes) ^ " changes, " ^
+          string_of_int (! failed_matches) ^ " matches failed")
+      else ();
+  in post_ast end;
 
 
 (* normalize_ast *)

--- a/src/Pure/Syntax/syntax.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -394,11 +394,12 @@
     fun show_pt pt =
       Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
   in
-    conditional (length pts > ! ambiguity_level) (fn () =>
+    if length pts > ! ambiguity_level then
       if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
       else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
           "produces " ^ string_of_int (length pts) ^ " parse trees.");
-         List.app (warning o show_pt) pts));
+         List.app (warning o show_pt) pts)
+    else ();
     SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
   end;
 

--- a/src/Pure/Thy/present.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/Thy/present.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -305,8 +305,8 @@
 
       val (doc_prefix1, documents) =
         if doc = "" then (NONE, [])
-        else if not (File.exists document_path) then (conditional verbose (fn () =>
-          std_error "Warning: missing document directory\n"); (NONE, []))
+        else if not (File.exists document_path) then
+          (if verbose then std_error "Warning: missing document directory\n" else (); (NONE, []))
         else (SOME (Path.append html_prefix document_path, html_prefix),
           read_versions doc_versions);
 
@@ -341,10 +341,10 @@
       " 2>&1" ^ (if verbose then "" else " >/dev/null");
     val doc_path = Path.append result_path (Path.ext format (Path.basic name));
   in
-    conditional verbose (fn () => writeln s);
+    if verbose then writeln s else ();
     system s;
-    conditional (not (File.exists doc_path)) (fn () =>
-      error ("No document: " ^ quote (show_path doc_path)));
+    File.exists doc_path orelse
+      error ("No document: " ^ quote (show_path doc_path));
     doc_path
   end;
 
@@ -399,7 +399,7 @@
       write_tex_index tex_index path;
       List.app (finish_tex path) thys);
   in
-    conditional info (fn () =>
+    if info then
      (File.mkdir (Path.append html_prefix session_path);
       Buffer.write (Path.append html_prefix pre_index_path) html_index;
       File.write (Path.append html_prefix session_entries_path) "";
@@ -413,12 +413,12 @@
       File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
       List.app finish_html thys;
       List.app (uncurry File.write) files;
-      conditional verbose (fn () =>
-        std_error ("Browser info at " ^ show_path html_prefix ^ "\n"))));
+      if verbose then std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
+    else ();
 
     (case doc_prefix2 of NONE => () | SOME (cp, path) =>
      (prepare_sources cp path;
-      conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));
+      if verbose then std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
 
     (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
       documents |> List.app (fn (name, tags) =>
@@ -426,7 +426,7 @@
          val _ = prepare_sources true path;
          val doc_path = isatool_document true doc_format name tags path result_path;
        in
-         conditional verbose (fn () => std_error ("Document at " ^ show_path doc_path ^ "\n"))
+         if verbose then std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
        end));
 
     browser_info := empty_browser_info;

--- a/src/Pure/Tools/codegen_data.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/Tools/codegen_data.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -426,8 +426,10 @@
   let
     val k = serial ();
     val kind = {name = name, empty = empty, merge = merge, purge = purge};
-    val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
-      warning ("Duplicate declaration of code data " ^ quote name));
+    val _ =
+      if Datatab.exists (equal name o #name o #2) (! kinds) then
+        warning ("Duplicate declaration of code data " ^ quote name)
+      else ();
     val _ = change kinds (Datatab.update (k, kind));
   in k end;
 

--- a/src/Pure/context.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/context.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -145,8 +145,10 @@
   let
     val k = serial ();
     val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
-    val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
-      warning ("Duplicate declaration of theory data " ^ quote name));
+    val _ =
+      if Datatab.exists (equal name o #name o #2) (! kinds) then
+        warning ("Duplicate declaration of theory data " ^ quote name)
+      else ();
     val _ = change kinds (Datatab.update (k, kind));
   in k end;
 
@@ -554,8 +556,10 @@
   let
     val k = serial ();
     val kind = {name = name, init = init};
-    val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
-      warning ("Duplicate declaration of proof data " ^ quote name));
+    val _ =
+      if Datatab.exists (equal name o #name o #2) (! kinds) then
+        warning ("Duplicate declaration of proof data " ^ quote name)
+      else ();
     val _ = change kinds (Datatab.update (k, kind));
   in k end;
 

--- a/src/Pure/library.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/library.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -75,7 +75,6 @@
   val toggle: bool ref -> bool
   val change: 'a ref -> ('a -> 'a) -> unit
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
-  val conditional: bool -> (unit -> unit) -> unit
 
   (*lists*)
   exception UnequalLengths
@@ -395,11 +394,6 @@
   in release result end;
 
 
-(* conditional execution *)
-
-fun conditional b f = if b then f () else ();
-
-
 
 (** lists **)
 

--- a/src/Pure/meta_simplifier.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -993,8 +993,10 @@
                  val b = Name.bound (#1 bounds);
                  val (v, t') = Thm.dest_abs (SOME b) t0;
                  val b' = #1 (Term.dest_Free (Thm.term_of v));
-                 val _ = conditional (b <> b') (fn () =>
-                   warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b'));
+                 val _ =
+                   if b <> b' then
+                     warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
+                   else ();
                  val ss' = add_bound ((b', T), a) ss;
                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
              in case botc skel' ss' t' of
@@ -1171,18 +1173,20 @@
 
 val debug_bounds = ref false;
 
-fun check_bounds ss ct = conditional (! debug_bounds) (fn () =>
-  let
-    val Simpset ({bounds = (_, bounds), ...}, _) = ss;
-    val bs = fold_aterms (fn Free (x, _) =>
-        if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
-        then insert (op =) x else I
-      | _ => I) (term_of ct) [];
-  in
-    if null bs then ()
-    else print_term true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) ss
-      (Thm.theory_of_cterm ct) (Thm.term_of ct)
-  end);
+fun check_bounds ss ct =
+  if ! debug_bounds then
+    let
+      val Simpset ({bounds = (_, bounds), ...}, _) = ss;
+      val bs = fold_aterms (fn Free (x, _) =>
+          if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
+          then insert (op =) x else I
+        | _ => I) (term_of ct) [];
+    in
+      if null bs then ()
+      else print_term true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) ss
+        (Thm.theory_of_cterm ct) (Thm.term_of ct)
+    end
+  else ();
 
 fun rewrite_cterm mode prover raw_ss raw_ct =
   let
@@ -1190,8 +1194,10 @@
     val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
     val ss = fallback_context thy raw_ss;
     val _ = inc simp_depth;
-    val _ = conditional (!simp_depth mod 20 = 0) (fn () =>
-      warning ("Simplification depth " ^ string_of_int (! simp_depth)));
+    val _ =
+      if ! simp_depth mod 20 = 0 then
+        warning ("Simplification depth " ^ string_of_int (! simp_depth))
+      else ();
     val _ = trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ss ct;
     val _ = check_bounds ss ct;
     val res = bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct

--- a/src/ZF/Tools/inductive_package.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -148,8 +148,10 @@
   val big_rec_name = Sign.intern_const thy big_rec_base_name;
 
 
-  val dummy = conditional verbose (fn () =>
-    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name));
+  val _ =
+    if verbose then
+      writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name)
+    else ();
 
   (*Forbid the inductive definition structure from clashing with a theory
     name.  This restriction may become obsolete as ML is de-emphasized.*)