# HG changeset patch # User huffman # Date 1267324312 28800 # Node ID b20501588930e943131dbe03aefeaa30de8ada91 # Parent f5461b02d754560bc337db607bd2e55b35d573b6 register match functions from domain_constructors.ML diff -r f5461b02d754 -r b20501588930 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Feb 27 18:09:11 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Feb 27 18:31:52 2010 -0800 @@ -133,14 +133,6 @@ fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; -fun add_matchers (((dname,_),cons) : eq) thy = - let - val con_names = map first cons; - val mat_names = map mat_name con_names; - fun qualify n = Sign.full_name thy (Binding.name n); - val ms = map qualify con_names ~~ map qualify mat_names; - in Fixrec.add_matchers ms thy end; - fun add_axioms definitional comp_dnam (eqs : eq list) thy' = let val comp_dname = Sign.full_bname thy' comp_dnam; @@ -209,7 +201,6 @@ |> Sign.add_path comp_dnam |> add_defs_infer ((*bisim_def::*)(if use_copy_def then [copy_def] else [])) |> Sign.parent_path - |> fold add_matchers eqs end; (* let (add_axioms) *) end; (* struct *) diff -r f5461b02d754 -r b20501588930 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 18:09:11 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 18:31:52 2010 -0800 @@ -947,6 +947,14 @@ define_consts (map_index mat_eqn (bindings ~~ spec)) thy end; + (* register match combinators with fixrec package *) + local + val con_names = map (fst o dest_Const o fst) spec; + val mat_names = map (fst o dest_Const) match_consts; + in + val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy; + end; + in (match_defs, thy) (* @@ -997,6 +1005,7 @@ case_def con_betas casedist iso_locale thy end; + (* qualify constants and theorems with domain name *) (* TODO: enable this earlier *) val thy = Sign.add_path dname thy;