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/Pure/Isar/local_defs.ML
changeset 33519 e31a85f92ce9
parent 33385 fb2358edcfb6
child 35624 c4e29a0bb8c1 
--- a/src/Pure/Isar/local_defs.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -186,12 +186,12 @@
 
 (* transformation rules *)
 
-structure Rules = GenericDataFun
+structure Rules = Generic_Data
 (
   type T = thm list;
-  val empty = []
+  val empty = [];
   val extend = I;
-  fun merge _ = Thm.merge_thms;
+  val merge = Thm.merge_thms;
 );
 
 fun print_rules ctxt =
isabelle