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