src/Tools/Compute_Oracle/compute.ML

     (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem
     (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem
 
     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 *)
 structure Encode :>