diff -r 91d06b04951f -r 84b5c89b8b49 src/Tools/Compute_Oracle/Compute_Oracle.thy
--- a/src/Tools/Compute_Oracle/Compute_Oracle.thy	Mon Jul 09 11:44:23 2007 +0200
+++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Mon Jul 09 17:36:25 2007 +0200
@@ -5,28 +5,10 @@
 Steven Obua's evaluator.
 *)
 
-theory Compute_Oracle
-imports CPure
-uses
-  "am_interpreter.ML"
-  "am_compiler.ML"
-  "am_util.ML"
-  "compute.ML"
+theory Compute_Oracle imports CPure
+uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "compute.ML" "linker.ML"
 begin
 
-oracle compute_oracle ("Compute.computer * (int -> string) * cterm") =
-  {* Compute.oracle_fn *}
-
-ML {*
-structure Compute =
-struct
-  open Compute
+setup {* Compute.setup; *}
 
-  fun rewrite_param r n ct =
-    compute_oracle (Thm.theory_of_cterm ct) (r, n, ct)
-
-  fun rewrite r ct = rewrite_param r default_naming ct
-end
-*}
-
-end
+end
\ No newline at end of file