src/HOL/Tools/recfun_codegen.ML
changeset 16424 18a07ad8fea8
parent 15700 970e0293dfb3
child 16645 a152d6b21c31
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Jun 17 18:33:03 2005 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri Jun 17 18:33:05 2005 +0200
     1.3 @@ -16,18 +16,17 @@
     1.4  
     1.5  open Codegen;
     1.6  
     1.7 -structure CodegenArgs =
     1.8 -struct
     1.9 +structure CodegenData = TheoryDataFun
    1.10 +(struct
    1.11    val name = "HOL/recfun_codegen";
    1.12    type T = thm list Symtab.table;
    1.13    val empty = Symtab.empty;
    1.14    val copy = I;
    1.15 -  val prep_ext = I;
    1.16 -  val merge = Symtab.merge_multi' Drule.eq_thm_prop;
    1.17 +  val extend = I;
    1.18 +  fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop;
    1.19    fun print _ _ = ();
    1.20 -end;
    1.21 +end);
    1.22  
    1.23 -structure CodegenData = TheoryDataFun(CodegenArgs);
    1.24  
    1.25  val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    1.26  val lhs_of = fst o dest_eqn o prop_of;