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/HOL/Tools/Function/partial_function.ML
changeset 41472 f6ab14e61604
parent 41117 d6379876ec4c
child 42083 e1209fc7ecdc 
--- a/src/HOL/Tools/Function/partial_function.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -27,7 +27,7 @@
   type T = ((term * term) * thm) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
-  fun merge (a, b) = Symtab.merge (K true) (a, b);
+  fun merge data = Symtab.merge (K true) data;
 )
 
 fun init fixp mono fixp_eq phi =
isabelle