src/HOL/Tools/record.ML

     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
   in
     thy
     |> Class.instantiation ([tyco], vs, sort)
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition NONE [] ((Binding.concealed Binding.empty, []), eq))
+    |-> (fn eq => Specification.definition NONE [] [] ((Binding.concealed Binding.empty, []), eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;
 
 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =

       thy
       |> Code.add_datatype [ext]
       |> fold Code.add_default_eqn simps
       |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
       |> `(fn lthy => Syntax.check_term lthy eq)
-      |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
+      |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
       |-> (fn (_, (_, eq_def)) =>
          Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
       |-> (fn eq_def => fn thy =>
             thy
             |> Code.del_eqn eq_def