src/HOL/Tools/record.ML
changeset 32770 c6e6a4665ff5
parent 32767 2885e2a09f72
child 32799 7478ea535416
     1.1 --- a/src/HOL/Tools/record.ML	Wed Sep 30 00:17:06 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Sep 30 00:27:19 2009 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4    val empty = Symtab.make [tuple_istuple];
     1.5    val copy = I;
     1.6    val extend = I;
     1.7 -  val merge = K (Symtab.merge Thm.eq_thm_prop);
     1.8 +  fun merge _ = Symtab.merge Thm.eq_thm_prop;
     1.9  );
    1.10  
    1.11  fun do_typedef name repT alphas thy =