diff -r d4dc5dc2db98 -r c121834a8808 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Sep 01 18:17:38 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Sep 01 18:17:40 2007 +0200
@@ -751,7 +751,7 @@
          singleton (ProofContext.export
            (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
            (rotate_prems ~1 (ObjectLogic.rulify (rule_by_tactic
-             (rewrite_tac [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] THEN
+             (rewrite_tac [le_fun_def, le_bool_def, @{thm sup_fun_eq}, @{thm sup_bool_eq}] THEN
                fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct)))))
        else
          prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def