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