src/Pure/Isar/generic_target.ML

--- a/src/Pure/Isar/generic_target.ML	Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Jun 23 11:01:14 2016 +0200
@@ -243,7 +243,7 @@
     (*local definition*)
     val ([(lhs, (_, local_def))], lthy3) = lthy2
       |> Context_Position.set_visible false
-      |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))]
+      |> Local_Defs.define [((b, NoSyn), (Binding.empty_atts, lhs'))]
       ||> Context_Position.restore_visible lthy2;
 
     (*result*)