--- a/src/HOL/Tools/record.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/record.ML Thu Apr 28 09:43:11 2016 +0200
@@ -1734,7 +1734,7 @@
thy
|> Class.instantiation ([tyco], vs, sort)
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (apfst Binding.concealed Attrib.empty_binding, eq)))
+ |-> (fn eq => Specification.definition NONE [] ((Binding.concealed Binding.empty, []), eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
@@ -1781,8 +1781,7 @@
|> 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 =>