# HG changeset patch
# User wenzelm
# Date 1255634919 -7200
# Node ID 5d5e123443b3a175f6fcaaf8c01e47c5f15ad179
# Parent  aa6c470a962a95c83dd6c9ca6191d95d3c681a11
normalized aliases of Output operations;

diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/SMT/Tools/smt_monomorph.ML
--- a/src/HOL/SMT/Tools/smt_monomorph.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_monomorph.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -112,7 +112,7 @@
       in
         if null is' then ts'
         else if count > monomorph_limit then
-          (Output.warning "monomorphization limit reached"; ts')
+          (warning "monomorphization limit reached"; ts')
         else mono (count + 1) is' ces' cs' ts'
       end
   in mono 0 (consts_of ms) (map (K []) rps) [] ms end
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -84,7 +84,7 @@
 val (trace, setup_trace) = Attrib.config_bool "smt_trace" false
 
 fun trace_msg ctxt f x =
-  if Config.get ctxt trace then Output.tracing (f x) else ()
+  if Config.get ctxt trace then tracing (f x) else ()
 
 
 (* interface to external solvers *)
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/Tools/Function/fundef_datatype.ML
--- a/src/HOL/Tools/Function/fundef_datatype.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -247,7 +247,7 @@
         fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
                     
         val (tss', _) = chop (length origs) tss
-        fun check (t, []) = (Output.warning (msg t); [])
+        fun check (t, []) = (warning (msg t); [])
           | check (t, s) = s
     in
         (map check (origs ~~ tss'); tss)
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/Tools/Function/induction_scheme.ML
--- a/src/HOL/Tools/Function/induction_scheme.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -355,7 +355,7 @@
   let
     val (ctxt', _, cases, concl) = dest_hhf ctxt t
     val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
-(*     val _ = Output.tracing (makestring scheme)*)
+(*     val _ = tracing (makestring scheme)*)
     val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
     val R = Free (Rn, mk_relT ST)
     val x = Free (xn, ST)
@@ -378,7 +378,7 @@
           indthm |> Drule.instantiate' [] [SOME inst]
                  |> simplify SumTree.sumcase_split_ss
                  |> Conv.fconv_rule ind_rulify
-(*                 |> (fn thm => (Output.tracing (makestring thm); thm))*)
+(*                 |> (fn thm => (tracing (makestring thm); thm))*)
         end                  
 
     val res = Conjunction.intr_balanced (map_index project branches)
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -39,7 +39,7 @@
 struct
 
 val PROFILE = FundefCommon.PROFILE
-fun TRACE x = if ! FundefCommon.profile then Output.tracing x else ()
+fun TRACE x = if ! FundefCommon.profile then tracing x else ()
 
 open ScnpSolve
 
@@ -316,17 +316,17 @@
     fun index xs = (1 upto length xs) ~~ xs
     fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
     val ims = index (map index ms)
-    val _ = Output.tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
+    val _ = tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
     fun print_call (k, c) =
       let
         val (_, p, _, q, _, _) = dest_call D c
-        val _ = Output.tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^ 
+        val _ = tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^ 
                                 Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
         val caller_ms = nth ms p
         val callee_ms = nth ms q
         val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
         fun print_ln (i : int, l) = concat (Int.toString i :: "   " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
-        val _ = Output.tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
+        val _ = tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
                                         " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n" 
                                 ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
       in
@@ -335,7 +335,7 @@
     fun list_call (k, c) =
       let
         val (_, p, _, q, _, _) = dest_call D c
-        val _ = Output.tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
+        val _ = tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
                                 Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^ 
                                 (Syntax.string_of_term ctxt c))
       in true end
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -415,7 +415,7 @@
         rewrite concl frees'
         |> map (fn (concl'::conclprems, _) =>
           Logic.list_implies ((flat prems') @ conclprems, concl')))
-    val _ = Output.tracing ("intro_ts': " ^
+    val _ = tracing ("intro_ts': " ^
       commas (map (Syntax.string_of_term_global thy) intro_ts'))
   in
     map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -27,7 +27,7 @@
     val (prednames, funnames) = List.partition (is_pred thy) constnames
     (* untangle recursion by defining predicates for all functions *)
     val _ = priority "Compiling functions to predicates..."
-    val _ = Output.tracing ("funnames: " ^ commas funnames)
+    val _ = tracing ("funnames: " ^ commas funnames)
     val thy' =
       thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates
       (get_specs funnames)
@@ -54,10 +54,10 @@
 
 fun preprocess const thy =
   let
-    val _ = Output.tracing ("Fetching definitions from theory...")
+    val _ = tracing ("Fetching definitions from theory...")
     val table = Pred_Compile_Data.make_const_spec_table thy
     val gr = Pred_Compile_Data.obtain_specification_graph table const
-    val _ = Output.tracing (commas (Graph.all_succs gr [const]))
+    val _ = tracing (commas (Graph.all_succs gr [const]))
     val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
   in fold_rev (preprocess_strong_conn_constnames gr)
     (Graph.strong_conn gr) thy
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -118,10 +118,10 @@
 
 (* debug stuff *)
 
-fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
+fun tracing s = (if ! Toplevel.debug then tracing s else ());
 
 fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
-fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
+fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *)
 
 val do_proofs = Unsynchronized.ref true;
 
@@ -407,7 +407,7 @@
      
 (* diagnostic display functions *)
 
-fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
+fun print_modes modes = tracing ("Inferred modes:\n" ^
   cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
     string_of_mode ms)) modes));
 
@@ -417,7 +417,7 @@
       ^ (string_of_entry pred mode entry)  
     fun print_pred (pred, modes) =
       "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
-    val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
+    val _ = tracing (cat_lines (map print_pred pred_mode_table))
   in () end;
 
 fun string_of_moded_prem thy (Prem (ts, p), tmode) =
@@ -498,7 +498,7 @@
 
 fun preprocess_elim thy nparams elimrule =
   let
-    val _ = Output.tracing ("Preprocessing elimination rule "
+    val _ = tracing ("Preprocessing elimination rule "
       ^ (Display.string_of_thm_global thy elimrule))
     fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
        HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
@@ -515,12 +515,12 @@
      end
     val cases' = map preprocess_case (tl prems)
     val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
-    (*val _ =  Output.tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*)
+    (*val _ =  tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*)
     val bigeq = (Thm.symmetric (Conv.implies_concl_conv
       (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
         (cterm_of thy elimrule')))
     (*
-    val _ = Output.tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq))   
+    val _ = tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq))   
     val res = 
     Thm.equal_elim bigeq elimrule
     *)
@@ -528,7 +528,7 @@
     val t = (fn {...} => mycheat_tac thy 1)
     val eq = Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) t
     *)
-    val _ = Output.tracing "Preprocessed elimination rule"
+    val _ = tracing "Preprocessed elimination rule"
   in
     Thm.equal_elim bigeq elimrule
   end;
@@ -657,8 +657,8 @@
 fun register_intros pre_intros thy =
   let
     val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
-    val _ = Output.tracing ("Registering introduction rules of " ^ c)
-    val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
+    val _ = tracing ("Registering introduction rules of " ^ c)
+    val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
     val nparams = guess_nparams T
     val pre_elim = 
       (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
@@ -1029,8 +1029,8 @@
 fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
   let
     (*
-  val _ = Output.tracing ("param_vs:" ^ commas param_vs)
-  val _ = Output.tracing ("iss:" ^
+  val _ = tracing ("param_vs:" ^ commas param_vs)
+  val _ = tracing ("iss:" ^
     commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
     *)
     val modes' = modes @ List.mapPartial
@@ -1058,7 +1058,7 @@
                       SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
                         (vs union generator_vs) ps
                     | NONE => let
-                    val _ = Output.tracing ("ps:" ^ (commas
+                    val _ = tracing ("ps:" ^ (commas
                     (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
                   in (*error "mode analysis failed"*)NONE end
                   end)
@@ -1088,9 +1088,9 @@
   in (p, List.filter (fn m => case find_index
     (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
       ~1 => true
-    | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
+    | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
       p ^ " violates mode " ^ string_of_mode m);
-        Output.tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
+        tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
   end;
 
 fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
@@ -2181,23 +2181,23 @@
 
 fun add_equations_of steps prednames thy =
   let
-    val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
-    val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+    val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+    val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
     val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
       prepare_intrs thy prednames
-    val _ = Output.tracing "Infering modes..."
+    val _ = tracing "Infering modes..."
     val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses 
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = print_modes modes
     val _ = print_moded_clauses thy moded_clauses
-    val _ = Output.tracing "Defining executable functions..."
+    val _ = tracing "Defining executable functions..."
     val thy' = fold (#create_definitions steps preds) modes thy
       |> Theory.checkpoint
-    val _ = Output.tracing "Compiling equations..."
+    val _ = tracing "Compiling equations..."
     val compiled_terms =
       (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
     val _ = print_compiled_terms thy' compiled_terms
-    val _ = Output.tracing "Proving equations..."
+    val _ = tracing "Proving equations..."
     val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
       moded_clauses compiled_terms
     val qname = #qname steps
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -725,7 +725,7 @@
           (* check this.  However, getting this really right seems   *)
           (* difficult because the user may state arbitrary axioms,  *)
           (* which could interact with overloading to create loops.  *)
-          ((*Output.tracing (" unfolding: " ^ axname);*)
+          ((*tracing (" unfolding: " ^ axname);*)
            unfold_loop rhs)
         | NONE => t)
       | Free _           => t
@@ -765,20 +765,14 @@
 
   fun collect_axioms thy t =
   let
-    val _ = Output.tracing "Adding axioms..."
-    (* (string * Term.term) list *)
+    val _ = tracing "Adding axioms..."
     val axioms = Theory.all_axioms_of thy
-    (* string * Term.term -> Term.term list -> Term.term list *)
     fun collect_this_axiom (axname, ax) axs =
     let
       val ax' = unfold_defs thy ax
     in
-      if member (op aconv) axs ax' then
-        axs
-      else (
-        Output.tracing axname;
-        collect_term_axioms (ax' :: axs, ax')
-      )
+      if member (op aconv) axs ax' then axs
+      else (tracing axname; collect_term_axioms (ax' :: axs, ax'))
     end
     (* Term.term list * Term.typ -> Term.term list *)
     and collect_sort_axioms (axs, T) =
@@ -939,7 +933,7 @@
         (collect_term_axioms (axs, t1), t2)
     (* Term.term list *)
     val result = map close_form (collect_term_axioms ([], t))
-    val _ = Output.tracing " ...done."
+    val _ = tracing " ...done."
   in
     result
   end;
@@ -1157,13 +1151,12 @@
     let
       val timer  = Timer.startRealTimer ()
       val u      = unfold_defs thy t
-      val _      = Output.tracing ("Unfolded term: " ^
-                                   Syntax.string_of_term_global thy u)
+      val _      = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
       val axioms = collect_axioms thy u
       (* Term.typ list *)
       val types = Library.foldl (fn (acc, t') =>
         acc union (ground_types thy t')) ([], u :: axioms)
-      val _     = Output.tracing ("Ground types: "
+      val _     = tracing ("Ground types: "
         ^ (if null types then "none."
            else commas (map (Syntax.string_of_typ_global thy) types)))
       (* we can only consider fragments of recursive IDTs, so we issue a  *)
@@ -1198,7 +1191,7 @@
         val init_model = (universe, [])
         val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
           bounds = [], wellformed = True}
-        val _          = Output.tracing ("Translating term (sizes: "
+        val _ = tracing ("Translating term (sizes: "
           ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
         (* translate 'u' and all axioms *)
         val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') =>
@@ -1216,31 +1209,31 @@
         val fm_ax = PropLogic.all (map toTrue (tl intrs))
         val fm    = PropLogic.all [#wellformed args, fm_ax, fm_u]
       in
-        Output.priority "Invoking SAT solver...";
+        priority "Invoking SAT solver...";
         (case SatSolver.invoke_solver satsolver fm of
           SatSolver.SATISFIABLE assignment =>
-          (Output.priority ("*** Model found: ***\n" ^ print_model thy model
+          (priority ("*** Model found: ***\n" ^ print_model thy model
             (fn i => case assignment i of SOME b => b | NONE => true));
            if maybe_spurious then "potential" else "genuine")
         | SatSolver.UNSATISFIABLE _ =>
-          (Output.priority "No model exists.";
+          (priority "No model exists.";
           case next_universe universe sizes minsize maxsize of
             SOME universe' => find_model_loop universe'
-          | NONE           => (Output.priority
+          | NONE           => (priority
             "Search terminated, no larger universe within the given limits.";
             "none"))
         | SatSolver.UNKNOWN =>
-          (Output.priority "No model found.";
+          (priority "No model found.";
           case next_universe universe sizes minsize maxsize of
             SOME universe' => find_model_loop universe'
-          | NONE           => (Output.priority
+          | NONE           => (priority
             "Search terminated, no larger universe within the given limits.";
             "unknown"))
         ) handle SatSolver.NOT_CONFIGURED =>
           (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
            "unknown")
       end handle MAXVARS_EXCEEDED =>
-        (Output.priority ("Search terminated, number of Boolean variables ("
+        (priority ("Search terminated, number of Boolean variables ("
           ^ string_of_int maxvars ^ " allowed) exceeded.");
           "unknown")
         val outcome_code = find_model_loop (first_universe types sizes minsize)
@@ -1262,14 +1255,14 @@
       maxtime>=0 orelse
         error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
       (* enter loop with or without time limit *)
-      Output.priority ("Trying to find a model that "
+      priority ("Trying to find a model that "
         ^ (if negate then "refutes" else "satisfies") ^ ": "
         ^ Syntax.string_of_term_global thy t);
       if maxtime>0 then (
         TimeLimit.timeLimit (Time.fromSeconds maxtime)
           wrapper ()
         handle TimeLimit.TimeOut =>
-          Output.priority ("Search terminated, time limit (" ^
+          priority ("Search terminated, time limit (" ^
             string_of_int maxtime
             ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")
       ) else
diff -r aa6c470a962a -r 5d5e123443b3 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Thu Oct 15 21:28:39 2009 +0200
@@ -106,10 +106,10 @@
 
 (* debug stuff *)
 
-fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
+fun tracing s = (if ! Toplevel.debug then tracing s else ());
 
 fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
-fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
+fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *)
 
 val do_proofs = Unsynchronized.ref true;
 
@@ -344,7 +344,7 @@
      
 (* diagnostic display functions *)
 
-fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
+fun print_modes modes = tracing ("Inferred modes:\n" ^
   cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
     string_of_mode ms)) modes));
 
@@ -354,7 +354,7 @@
       ^ (string_of_entry pred mode entry)  
     fun print_pred (pred, modes) =
       "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
-    val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
+    val _ = tracing (cat_lines (map print_pred pred_mode_table))
   in () end;
 
 fun string_of_moded_prem thy (Prem (ts, p), tmode) =
@@ -1002,7 +1002,7 @@
   in (p, List.filter (fn m => case find_index
     (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
       ~1 => true
-    | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
+    | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
       p ^ " violates mode " ^ string_of_mode m); false)) ms)
   end;
 
@@ -1915,22 +1915,22 @@
 
 fun add_equations_of steps prednames thy =
   let
-    val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+    val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
     val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) =
       prepare_intrs thy prednames
-    val _ = Output.tracing "Infering modes..."
+    val _ = tracing "Infering modes..."
     val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses 
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = print_modes modes
     val _ = print_moded_clauses thy moded_clauses
-    val _ = Output.tracing "Defining executable functions..."
+    val _ = tracing "Defining executable functions..."
     val thy' = fold (#create_definitions steps preds) modes thy
       |> Theory.checkpoint
-    val _ = Output.tracing "Compiling equations..."
+    val _ = tracing "Compiling equations..."
     val compiled_terms =
       (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
     val _ = print_compiled_terms thy' compiled_terms
-    val _ = Output.tracing "Proving equations..."
+    val _ = tracing "Proving equations..."
     val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
       moded_clauses compiled_terms
     val qname = #qname steps