diff -r 2c8caac48ade -r dffe405b090d src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Sun Oct 21 14:21:48 2007 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sun Oct 21 14:21:53 2007 +0200
@@ -98,7 +98,7 @@
     val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
     val (fixdef_thms, thy') =
       PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
-    val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;
+    val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms;
     
     val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
     val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold
@@ -110,8 +110,8 @@
     fun unfolds [] thm = []
       | unfolds (n::[]) thm = [(n^"_unfold", thm)]
       | unfolds (n::ns) thm = let
-          val thmL = thm RS cpair_eqD1;
-          val thmR = thm RS cpair_eqD2;
+          val thmL = thm RS @{thm cpair_eqD1};
+          val thmR = thm RS @{thm cpair_eqD2};
         in (n^"_unfold", thmL) :: unfolds ns thmR end;
     val unfold_thms = unfolds names ctuple_unfold_thm;
     val thms = ctuple_induct_thm :: unfold_thms;
@@ -210,7 +210,7 @@
 (* proves a block of pattern matching equations as theorems, using unfold *)
 fun make_simps thy (unfold_thm, eqns) =
   let
-    val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1];
+    val tacs = [rtac (unfold_thm RS @{thm ssubst_lhs}) 1, asm_simp_tac (simpset_of thy) 1];
     fun prove_term t = Goal.prove_global thy [] [] t (K (EVERY tacs));
     fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
   in