src/Pure/Isar/expression.ML

     val asm' = Option.map (Morphism.term morph) asm;
     val defs' = map (Morphism.term morph) defs;
     val text' =
       text |>
        (if is_some asm then
-          eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
+          eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])])
         else I) |>
        (if not (null defs) then
-          eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
+          eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs'))
         else I)
 (* FIXME clone from locale.ML *)
   in text' end;
 
 fun eval_elem ctxt elem text =