src/Pure/Isar/local_defs.ML

     val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T));
   in
     state
     |> fix [([x], None)]
     |> Proof.match_bind_i [(pats, rhs)]
-    |> Proof.assm_i export_defs [(name, atts, [(Logic.mk_equals (lhs, rhs), ([], []))])]
+    |> Proof.assm_i export_defs [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
   end;
 
 val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats;
 val def_i = gen_def Proof.fix_i ProofContext.cert_term ProofContext.cert_term_pats;