src/Pure/Isar/spec_rules.ML
changeset 41472 f6ab14e61604
parent 34948 2d5f2a9f7601
child 42360 da8817d01e7c
--- a/src/Pure/Isar/spec_rules.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -37,7 +37,7 @@
         eq_list Thm.eq_thm_prop (ths1, ths2))
       (#1 o #2);
   val extend = I;
-  fun merge data = Item_Net.merge data;
+  val merge = Item_Net.merge;
 );
 
 val get = Item_Net.content o Rules.get o Context.Proof;