# HG changeset patch
# User wenzelm
# Date 1257883470 -3600
# Node ID 16a263d2b1c92b16691760f8545d5384641190ec
# Parent  89c43964696068196e440fd5480e0cb46a5901ec
adapted Theory_Data;

diff -r 89c439646960 -r 16a263d2b1c9 src/Tools/auto_counterexample.ML
--- a/src/Tools/auto_counterexample.ML	Tue Nov 10 21:02:18 2009 +0100
+++ b/src/Tools/auto_counterexample.ML	Tue Nov 10 21:04:30 2009 +0100
@@ -28,12 +28,12 @@
 
 (* configuration *)
 
-structure Data = TheoryDataFun(
+structure Data = Theory_Data
+(
   type T = (string * (Proof.state -> bool * Proof.state)) list
   val empty = []
-  val copy = I
   val extend = I
-  fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2)
+  fun merge data : T = AList.merge (op =) (K true) data
 )
 
 val register_tool = Data.map o AList.update (op =)