
diff -r 179ff9cb160b -r 5b25fee0362c src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOLCF/Fixrec.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -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




