src/HOLCF/Pcpo.thy
changeset 22577 1a08fce38565
parent 20713 823967ef47f1
child 25131 2c8caac48ade
--- a/src/HOLCF/Pcpo.thy	Tue Apr 03 19:31:48 2007 +0200
+++ b/src/HOLCF/Pcpo.thy	Wed Apr 04 00:10:59 2007 +0200
@@ -206,8 +206,7 @@
       | _ => SOME meta_UU_reorient;
 in
   val UU_reorient_simproc = 
-    Simplifier.simproc (the_context ())
-      "UU_reorient_simproc" ["UU=x"] reorient_proc
+    Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc
 end;
 
 Addsimprocs [UU_reorient_simproc];