src/CCL/Wfd.thy
changeset 31902 862ae16a799d
parent 30515 bca05b17b618
child 32211 752dbe71cc89
--- a/src/CCL/Wfd.thy	Thu Jul 02 17:33:36 2009 +0200
+++ b/src/CCL/Wfd.thy	Thu Jul 02 17:34:14 2009 +0200
@@ -495,7 +495,7 @@
 ML {*
 
 local
-  structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules");
+  structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
 in
 
 fun eval_tac ctxt ths =