src/Pure/Tools/codegen_package.ML
changeset 18708 4b3dadb4fe33
parent 18704 2c86ced392a8
child 18756 5eb3df798405
     1.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Pure/Tools/codegen_package.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -304,9 +304,11 @@
     1.4      target_data = Symtab.join (K (merge_target_data #> SOME))
     1.5        (target_data1, target_data2)
     1.6    };
     1.7 -  fun print thy _ = writeln "sorry, this stuff is too complicated...";
     1.8 +  fun print _ _ = ();
     1.9  end);
    1.10  
    1.11 +val _ = Context.add_setup CodegenData.init;
    1.12 +
    1.13  fun map_codegen_data f thy =
    1.14    case CodegenData.get thy
    1.15     of { modl, gens, target_data, logic_data } =>
    1.16 @@ -1311,18 +1313,17 @@
    1.17  
    1.18  
    1.19  
    1.20 -(** setup **)
    1.21 +(** theory setup **)
    1.22  
    1.23 -val _ = Context.add_setup [
    1.24 -  CodegenData.init,
    1.25 -(*   add_appconst_i ("op =", ((2, 2), appgen_eq)),  *)
    1.26 -  add_eqextr ("defs", eqextr_defs),
    1.27 -  add_defgen ("clsdecl", defgen_clsdecl),
    1.28 -  add_defgen ("funs", defgen_funs),
    1.29 -  add_defgen ("clsmem", defgen_clsmem),
    1.30 -  add_defgen ("datatypecons", defgen_datatypecons)(*,
    1.31 -  add_defgen ("clsinst", defgen_clsinst)  *)
    1.32 -];
    1.33 +val _ = Context.add_setup
    1.34 + (add_eqextr ("defs", eqextr_defs) #>
    1.35 +  add_defgen ("clsdecl", defgen_clsdecl) #>
    1.36 +  add_defgen ("funs", defgen_funs) #>
    1.37 +  add_defgen ("clsmem", defgen_clsmem) #>
    1.38 +  add_defgen ("datatypecons", defgen_datatypecons));
    1.39 +
    1.40 +(*   add_appconst_i ("op =", ((2, 2), appgen_eq))  *)
    1.41 +(*   add_defgen ("clsinst", defgen_clsinst)  *)
    1.42  
    1.43  end; (* local *)
    1.44