src/Tools/Compute_Oracle/compute.ML
changeset 25218 fcf0f50e478c
parent 25217 3224db6415ae
child 25520 e123c81257a5
--- 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 *)