--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Thu Jun 23 11:01:14 2016 +0200
@@ -298,8 +298,9 @@
EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt,
SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i;
val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
- val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
- [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
+ val (_, transfer_lthy) =
+ Proof_Context.note_thmss ""
+ [(Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
val f_alt_def = Goal.prove_sorry transfer_lthy [] [] f_alt_def_goal
(fn {context = ctxt, prems = _} => HEADGOAL (f_alt_def_tac ctxt))
|> Thm.close_derivation
@@ -444,9 +445,10 @@
(map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
rtac ctxt TrueI] i;
- val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
- [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
- (@{thms Domain_eq_top}, [Transfer.transfer_domain_add]) ])] lthy;
+ val (_, transfer_lthy) =
+ Proof_Context.note_thmss "" [(Binding.empty_atts,
+ [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
+ (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])])] lthy;
val quot_thm_isom = Goal.prove_sorry transfer_lthy [] [] typedef_goal
(fn {context = ctxt, prems = _} => typ_isom_tac ctxt 1)