--- a/src/CCL/Wfd.thy Sun May 06 21:50:17 2007 +0200
+++ b/src/CCL/Wfd.thy Mon May 07 00:49:59 2007 +0200
@@ -500,12 +500,10 @@
structure Data = GenericDataFun
(
- val name = "CCL/eval";
type T = thm list;
val empty = [];
val extend = I;
fun merge _ = Drule.merge_rules;
- fun print _ _ = ();
);
in
@@ -518,7 +516,6 @@
DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get (Context.Proof ctxt)) 1)) 1;
val eval_setup =
- Data.init #>
Attrib.add_attributes
[("eval", Attrib.add_del_args eval_add eval_del, "declaration of evaluation rule")] #>
Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>