--- a/src/HOLCF/Fixrec.thy Thu Feb 26 08:48:33 2009 -0800
+++ b/src/HOLCF/Fixrec.thy Thu Feb 26 10:28:53 2009 -0800
@@ -583,6 +583,20 @@
use "Tools/fixrec_package.ML"
+setup {* FixrecPackage.setup *}
+
+setup {*
+ FixrecPackage.add_matchers
+ [ (@{const_name up}, @{const_name match_up}),
+ (@{const_name sinl}, @{const_name match_sinl}),
+ (@{const_name sinr}, @{const_name match_sinr}),
+ (@{const_name spair}, @{const_name match_spair}),
+ (@{const_name cpair}, @{const_name match_cpair}),
+ (@{const_name ONE}, @{const_name match_ONE}),
+ (@{const_name TT}, @{const_name match_TT}),
+ (@{const_name FF}, @{const_name match_FF}) ]
+*}
+
hide (open) const return bind fail run cases
end