src/HOL/Tools/inductive.ML
changeset 35625 9c818cab0dd0
parent 35624 c4e29a0bb8c1
child 35646 b32d6c1bdb4d
     1.1 --- a/src/HOL/Tools/inductive.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -788,7 +788,7 @@
     1.4         else if coind then
     1.5           singleton (ProofContext.export
     1.6             (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
     1.7 -           (rotate_prems ~1 (ObjectLogic.rulify
     1.8 +           (rotate_prems ~1 (Object_Logic.rulify
     1.9               (fold_rule rec_preds_defs
    1.10                 (rewrite_rule simp_thms'''
    1.11                  (mono RS (fp_def RS @{thm def_coinduct}))))))