src/HOL/Tools/Lifting/lifting_def_code_dt.ML

             val f_alt_def_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (f_alt_def_goal_lhs, f_alt_def_goal_rhs));
             fun f_alt_def_tac ctxt i =
               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
               |> singleton (Variable.export lthy args_lthy)
             val lthy = args_lthy

           SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *), 
           Raw_Simplifier.rewrite_goal_tac ctxt 
           (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)
       |> Thm.close_derivation
       |> singleton (Variable.export transfer_lthy lthy)