src/HOL/Tools/record.ML
changeset 35625 9c818cab0dd0
parent 35615 61bb9f8af129
child 35742 eb8d2f668bfc
equal deleted inserted replaced
35624:c4e29a0bb8c1 35625:9c818cab0dd0
  2212         val ind =
  2212         val ind =
  2213           cterm_instantiate
  2213           cterm_instantiate
  2214             [(cterm_of defs_thy Pvar, cterm_of defs_thy
  2214             [(cterm_of defs_thy Pvar, cterm_of defs_thy
  2215               (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
  2215               (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
  2216             induct_scheme;
  2216             induct_scheme;
  2217         in ObjectLogic.rulify (mp OF [ind, refl]) end;
  2217         in Object_Logic.rulify (mp OF [ind, refl]) end;
  2218 
  2218 
  2219     val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
  2219     val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
  2220     val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
  2220     val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
  2221 
  2221 
  2222     fun cases_prf () =
  2222     fun cases_prf () =