--- a/src/HOL/Tools/datatype_realizer.ML Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Thu Mar 20 12:09:20 2008 +0100
@@ -123,7 +123,7 @@
[rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
rtac (cterm_instantiate inst induction) 1,
ALLGOALS ObjectLogic.atomize_prems_tac,
- rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
+ rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
REPEAT (etac allE i) THEN atac i)) 1)]);