--- a/src/HOL/Code_Generator.thy Wed May 09 07:53:04 2007 +0200
+++ b/src/HOL/Code_Generator.thy Wed May 09 07:53:06 2007 +0200
@@ -6,8 +6,16 @@
theory Code_Generator
imports HOL
+uses "~~/src/HOL/Tools/recfun_codegen.ML"
begin
+ML {*
+structure HOL =
+struct
+ val thy = theory "HOL";
+end;
+*} -- "belongs to theory HOL"
+
subsection {* SML code generator setup *}
types_code
@@ -55,6 +63,7 @@
in
Codegen.add_codegen "eq_codegen" eq_codegen
+#> RecfunCodegen.setup
end
*}
@@ -107,7 +116,7 @@
shows "(\<not> True) = False"
and "(\<not> False) = True" by (rule HOL.simp_thms)+
-lemmas [code func] = imp_conv_disj
+lemmas [code] = imp_conv_disj
lemmas [code func] = if_True if_False
@@ -174,7 +183,7 @@
oracle eval_oracle ("term") = {* fn thy => fn t =>
if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) []
then t
- else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
+ else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
*}
method_setup eval = {*