src/HOLCF/Tools/fixrec.ML

   val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
     -> (Attrib.binding * string) list -> local_theory -> local_theory
   val add_fixpat: Thm.binding * term list -> theory -> theory
   val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
   val add_matchers: (string * string) list -> theory -> theory
-  val fixrec_simp_add: Thm.attribute
-  val fixrec_simp_del: Thm.attribute
+  val fixrec_simp_add: attribute
+  val fixrec_simp_del: attribute
   val fixrec_simp_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
 end;
 
 structure Fixrec :> FIXREC =

 structure FixrecUnfoldData = GenericDataFun (
   type T = thm Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  val merge = K (Symtab.merge (K true));
+  fun merge _ = Symtab.merge (K true);
 );
 
 local
 
 fun name_of (Const (n, T)) = n

 val lhs_name =
   name_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
 
 in
 
-val add_unfold : Thm.attribute =
+val add_unfold : attribute =
   Thm.declaration_attribute
     (fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th)));
 
 end
 

 structure FixrecMatchData = TheoryDataFun (
   type T = string Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  val merge = K (Symtab.merge (K true));
+  fun merge _ = Symtab.merge (K true);
 );
 
 (* associate match functions with pattern constants *)
 fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
 

       addsimps simp_thms
       addsimps [@{thm beta_cfun}]
       addsimprocs [@{simproc cont_proc}];
   val copy = I;
   val extend = I;
-  val merge = K merge_ss;
+  fun merge _ = merge_ss;
 );
 
 fun fixrec_simp_tac ctxt =
   let
     val tab = FixrecUnfoldData.get (Context.Proof ctxt);

         val rule = unfold_thm RS @{thm ssubst_lhs};
       in
         CHANGED (rtac rule i THEN asm_simp_tac ss i)
       end
   in
-    SUBGOAL (fn ti => tac ti handle _ => no_tac)
-  end;
-
-val fixrec_simp_add : Thm.attribute =
+    SUBGOAL (fn ti => tac ti handle _ => no_tac)  (* FIXME avoid handle _ *)
+  end;
+
+val fixrec_simp_add : attribute =
   Thm.declaration_attribute
     (fn th => FixrecSimpData.map (fn ss => ss addsimps [th]));
 
-val fixrec_simp_del : Thm.attribute =
+val fixrec_simp_del : attribute =
   Thm.declaration_attribute
     (fn th => FixrecSimpData.map (fn ss => ss delsimps [th]));
 
 (* proves a block of pattern matching equations as theorems, using unfold *)
 fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =