src/HOL/Tools/Datatype/datatype_realizer.ML
changeset 37136 e0c9d3e49e15
parent 36744 6e1f3d609a68
child 37236 739d8b9c59da
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed May 26 16:05:25 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed May 26 16:05:25 2010 +0200
@@ -113,7 +113,7 @@
 
     val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
       (fn prems =>
-         [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
+         [rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
           rtac (cterm_instantiate inst induct) 1,
           ALLGOALS Object_Logic.atomize_prems_tac,
           rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),