src/HOL/Tools/record.ML
changeset 35625 9c818cab0dd0
parent 35615 61bb9f8af129
child 35742 eb8d2f668bfc
     1.1 --- a/src/HOL/Tools/record.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -2214,7 +2214,7 @@
     1.4              [(cterm_of defs_thy Pvar, cterm_of defs_thy
     1.5                (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
     1.6              induct_scheme;
     1.7 -        in ObjectLogic.rulify (mp OF [ind, refl]) end;
     1.8 +        in Object_Logic.rulify (mp OF [ind, refl]) end;
     1.9  
    1.10      val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
    1.11      val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;