# HG changeset patch
# User wenzelm
# Date 1307540395 -7200
# Node ID 1fd31f859fc796444bd81c2bf78a312b8471d215
# Parent  91bf67e0e755c44a1c7f184f59602420a002fcef
pervasive Output operations;

diff -r 91bf67e0e755 -r 1fd31f859fc7 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Jun 08 15:25:44 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Jun 08 15:39:55 2011 +0200
@@ -389,7 +389,7 @@
 fun mutate_theorem create_entry thy mtds thm =
   let
     val exec = is_executable_thm thy thm
-    val _ = Output.tracing (if exec then "EXEC" else "NOEXEC")
+    val _ = tracing (if exec then "EXEC" else "NOEXEC")
     val mutants =
           (if num_mutations = 0 then
              [Thm.prop_of thm]
diff -r 91bf67e0e755 -r 1fd31f859fc7 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Wed Jun 08 15:25:44 2011 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Wed Jun 08 15:39:55 2011 +0200
@@ -86,9 +86,9 @@
 fun warnings ctxt origs tss =
   let
     fun warn_redundant t =
-      Output.warning ("Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t))
+      warning ("Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t))
     fun warn_missing strs =
-      Output.warning (cat_lines ("Missing patterns in function definition:" :: strs))
+      warning (cat_lines ("Missing patterns in function definition:" :: strs))
 
     val (tss', added) = chop (length origs) tss
 
diff -r 91bf67e0e755 -r 1fd31f859fc7 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Jun 08 15:25:44 2011 +0200
+++ b/src/HOL/Tools/Function/function.ML	Wed Jun 08 15:39:55 2011 +0200
@@ -87,8 +87,7 @@
     val defname = mk_defname fixes
     val FunctionConfig {partials, default, ...} = config
     val _ =
-      if is_some default then Output.legacy_feature
-        "'function (default)'. Use 'partial_function'."
+      if is_some default then legacy_feature "'function (default)'. Use 'partial_function'."
       else ()
 
     val ((goal_state, cont), lthy') =
diff -r 91bf67e0e755 -r 1fd31f859fc7 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Jun 08 15:25:44 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Jun 08 15:39:55 2011 +0200
@@ -211,7 +211,7 @@
     | ths => rev ths
     val _ =
       if show_intermediate_results options then
-        Output.tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
+        tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
           commas (map (Display.string_of_thm_global thy) spec))
       else ()
   in
diff -r 91bf67e0e755 -r 1fd31f859fc7 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Wed Jun 08 15:25:44 2011 +0200
+++ b/src/Pure/Thy/term_style.ML	Wed Jun 08 15:39:55 2011 +0200
@@ -53,7 +53,7 @@
       >> fold I
   || Scan.succeed I));
 
-val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style.";
+val parse_bare = Args.context :|-- (fn ctxt => (legacy_feature "Old-style antiquotation style.";
   Scan.lift Args.liberal_name
   >> (fn name => fst (Args.context_syntax "style"
        (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
@@ -84,7 +84,7 @@
 fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
   let
     val i_str = string_of_int i;
-    val _ = Output.legacy_feature (quote ("prem" ^ i_str)
+    val _ = legacy_feature (quote ("prem" ^ i_str)
       ^ " term style encountered; use explicit argument syntax "
       ^ quote ("prem " ^ i_str) ^ " instead.");
     val prems = Logic.strip_imp_prems t;