--- a/src/HOL/Tools/recfun_codegen.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Fri Jun 17 18:33:05 2005 +0200
@@ -16,18 +16,17 @@
open Codegen;
-structure CodegenArgs =
-struct
+structure CodegenData = TheoryDataFun
+(struct
val name = "HOL/recfun_codegen";
type T = thm list Symtab.table;
val empty = Symtab.empty;
val copy = I;
- val prep_ext = I;
- val merge = Symtab.merge_multi' Drule.eq_thm_prop;
+ val extend = I;
+ fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop;
fun print _ _ = ();
-end;
+end);
-structure CodegenData = TheoryDataFun(CodegenArgs);
val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
val lhs_of = fst o dest_eqn o prop_of;