# HG changeset patch
# User huffman
# Date 1139017029 -3600
# Node ID 83acd39b1babb558472adaed6578ab41944aaa5c
# Parent  34f9df073ad962d616dd33d3e9f126bd13e7a25c
UU_reorient_simproc no longer rewrites UU = numeral

diff -r 34f9df073ad9 -r 83acd39b1bab src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Fri Feb 03 23:12:31 2006 +0100
+++ b/src/HOLCF/Pcpo.thy	Sat Feb 04 02:37:09 2006 +0100
@@ -197,10 +197,13 @@
 ML_setup {*
 local
   val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
-  fun is_UU (Const ("Pcpo.UU",_)) = true
-    | is_UU _ = false;
   fun reorient_proc sg _ (_ $ t $ u) =
-    if is_UU u then NONE else SOME meta_UU_reorient;
+    case u of
+        Const("Pcpo.UU",_) => NONE
+      | Const("0", _) => NONE
+      | Const("1", _) => NONE
+      | Const("Numeral.number_of", _) $ _ => NONE
+      | _ => SOME meta_UU_reorient;
 in
   val UU_reorient_simproc = 
     Simplifier.simproc (the_context ())