# 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]));