diff -r 3d3ebc0c927c -r 329f1b4d9d16 src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Thu Sep 20 12:09:09 2007 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML	Thu Sep 20 12:10:23 2007 +0200
@@ -25,10 +25,14 @@
 
     val setup : theory -> theory
 
+    val print_encoding : bool ref
+
 end
 
 structure Compute :> COMPUTE = struct
 
+val print_encoding = ref false
+
 datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML	 
 
 (* Terms are mapped to integer codes *)
@@ -261,8 +265,6 @@
 	      | HASKELL => ProgHaskell (AM_GHC.compile rules)
 	      | SML => ProgSML (AM_SML.compile rules)
 
-(*	val _ = print (Encode.fold (fn x => fn s => x::s) encoding [])*)
-
         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
 
 	val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
@@ -290,6 +292,7 @@
         val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct
         val thy = Theory.merge (Theory.deref rthy, ctthy)
         val (encoding, t) = report "remove_types" (fn () => remove_types encoding t)
+	val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()
         val t = report "run" (fn () => run prog t)
         val t = report "infer_types" (fn () => infer_types naming encoding ty t)
     in
@@ -340,7 +343,7 @@
 fun compute_oracle (thy, Param (r, naming, ct)) =
     let
         val _ = Theory.assert_super (theory_of r) thy
-        val t' = compute r naming ct
+        val t' = timeit (fn () => compute r naming ct)
 	val eq = Logic.mk_equals (term_of ct, t')
 	val hyps = hyps_of r
 	val shyptab = shyptab_of r