--- a/src/HOL/Tools/inductive_realizer.ML Wed May 26 16:05:25 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed May 26 16:05:25 2010 +0200
@@ -389,7 +389,7 @@
end) (rlzs ~~ rnames);
val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
(fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
- val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
+ val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
[rtac (#raw_induct ind_info) 1,
rewrite_goals_tac rews,