src/HOL/Tools/record.ML
changeset 38401 c4de81b7fdec
parent 38252 175a5b4b2c94
child 38529 4cc2ca4d6237
equal deleted inserted replaced
38400:9bfcb1507c6b 38401:c4de81b7fdec
  1215           else NONE
  1215           else NONE
  1216       | _ => NONE));
  1216       | _ => NONE));
  1217 
  1217 
  1218 fun get_upd_acc_cong_thm upd acc thy simpset =
  1218 fun get_upd_acc_cong_thm upd acc thy simpset =
  1219   let
  1219   let
  1220     val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)];
  1220     val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)];
  1221     val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
  1221     val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
  1222   in
  1222   in
  1223     Goal.prove (ProofContext.init_global thy) [] [] prop
  1223     Goal.prove (ProofContext.init_global thy) [] [] prop
  1224       (fn _ =>
  1224       (fn _ =>
  1225         simp_tac simpset 1 THEN
  1225         simp_tac simpset 1 THEN