--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Apr 28 09:43:11 2016 +0200
@@ -93,7 +93,7 @@
mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
|> Syntax.check_term lthy;
val ((_, (_, raw_def)), lthy') =
- Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
+ Specification.definition NONE [] (Attrib.empty_binding, spec) lthy;
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
in