src/HOL/Tools/Datatype/datatype_realizer.ML
changeset 35625 9c818cab0dd0
parent 35364 b8c62d60195c
child 35845 e5980f0ad025
     1.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4        (fn prems =>
     1.5           [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
     1.6            rtac (cterm_instantiate inst induct) 1,
     1.7 -          ALLGOALS ObjectLogic.atomize_prems_tac,
     1.8 +          ALLGOALS Object_Logic.atomize_prems_tac,
     1.9            rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
    1.10            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
    1.11              REPEAT (etac allE i) THEN atac i)) 1)]);