--- 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 *)
--- 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;