diff -r 3224db6415ae -r fcf0f50e478c src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Sat Oct 27 18:37:32 2007 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML	Sat Oct 27 18:37:33 2007 +0200
@@ -35,12 +35,16 @@
 
     val setup_compute : theory -> theory
 
+    val print_encoding : bool ref
+
 end
 
 structure Compute :> COMPUTE = struct
 
 open Report;
 
+val print_encoding = ref false
+
 datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML	 
 
 (* Terms are mapped to integer codes *)