src/HOL/Code_Generator.thy

 
 header {* Setup of code generator tools *}
 
 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
   "bool"  ("bool")

      | _ => NONE);
 
 in
 
 Codegen.add_codegen "eq_codegen" eq_codegen
+#> RecfunCodegen.setup
 
 end
 *}
 
 text {* Evaluation *}

 
 lemma [code func]:
   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
 
 instance bool :: eq ..
 

 subsection {* Evaluation oracle *}
 
 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 = {*
 let
   fun eval_tac thy =