Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/auto_counterexample.ML
changeset 33600 16a263d2b1c9
parent 33561 ab01b72715ef 
--- 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 =)
isabelle