--- 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