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