src/HOLCF/Tools/fixrec_package.ML

     val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint);
     
     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
           (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
                     simp_tac (simpset_of thy') 1]);

           (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind);
     
     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;
     val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy';
   in

 (*************************************************************************)
 
 (* 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
     map prove_eqn eqns
   end;