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