# HG changeset patch
# User wenzelm
# Date 1257436963 -3600
# Node ID 5d78b2bd27dee8a50a614ebf0469642bb4be09f9
# Parent  99a5f22a967df8ce4425830216145f0d63b544b4
made SML/NJ happy;
normalized type abbreviations;

diff -r 99a5f22a967d -r 5d78b2bd27de src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Thu Nov 05 16:10:49 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Thu Nov 05 17:02:43 2009 +0100
@@ -13,8 +13,8 @@
   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;
@@ -165,7 +165,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  val merge = K (Symtab.merge (K true));
+  fun merge _ = Symtab.merge (K true);
 );
 
 local
@@ -179,7 +179,7 @@
 
 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)));
 
@@ -257,7 +257,7 @@
   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 *)
@@ -372,7 +372,7 @@
       addsimprocs [@{simproc cont_proc}];
   val copy = I;
   val extend = I;
-  val merge = K merge_ss;
+  fun merge _ = merge_ss;
 );
 
 fun fixrec_simp_tac ctxt =
@@ -391,14 +391,14 @@
         CHANGED (rtac rule i THEN asm_simp_tac ss i)
       end
   in
-    SUBGOAL (fn ti => tac ti handle _ => no_tac)
+    SUBGOAL (fn ti => tac ti handle _ => no_tac)  (* FIXME avoid handle _ *)
   end;
 
-val fixrec_simp_add : Thm.attribute =
+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]));