src/HOLCF/Pcpo.thy

       | Const("HOL.one", _) => NONE
       | Const("Numeral.number_of", _) $ _ => NONE
       | _ => 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];
 *}