--- 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]
--- 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
--- 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') =
--- 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
--- 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;