src/HOL/Tools/Function/scnp_reconstruct.ML

 
 structure ScnpReconstruct : SCNP_RECONSTRUCT =
 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
 
 val natT = HOLogic.natT
 val nat_pairT = HOLogic.mk_prodT (natT, natT)

     val ms = map (get_measures D) (0 upto np - 1)
     val tys = map (get_types D) (0 upto np - 1)
     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
         true
       end
     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
     val _ = forall list_call ((1 upto length cs) ~~ cs)
     val _ = forall print_call ((1 upto length cs) ~~ cs)