--- a/src/HOL/Tools/inductive_codegen.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon May 07 00:49:59 2007 +0200
@@ -22,8 +22,7 @@
Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
structure CodegenData = TheoryDataFun
-(struct
- val name = "HOL/inductive_codegen";
+(
type T =
{intros : (thm * (string * int)) list Symtab.table,
graph : unit Graph.T,
@@ -37,8 +36,7 @@
{intros = merge_rules (intros1, intros2),
graph = Graph.merge (K true) (graph1, graph2),
eqns = merge_rules (eqns1, eqns2)};
- fun print _ _ = ();
-end);
+);
fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
@@ -653,7 +651,6 @@
val setup =
add_codegen "inductive" inductive_codegen #>
- CodegenData.init #>
add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);