--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Apr 28 09:43:11 2016 +0200
@@ -1829,7 +1829,7 @@
val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
- [(apfst Binding.concealed Attrib.empty_binding, parsed_eq)]
+ [(((Binding.concealed Binding.empty, []), parsed_eq), [])]
Function_Common.default_config pat_completeness_auto lthy;
in
((defname, (pelim, pinduct, psimp)), lthy)
@@ -1982,7 +1982,7 @@
val (plugins, friend, transfer) = get_options lthy opts;
val ([((b, fun_T), mx)], [(_, eq)]) =
- fst (Specification.read_spec raw_fixes [(Attrib.empty_binding, raw_eq)] lthy);
+ fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [])] lthy);
val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
error ("Type of " ^ Binding.print b ^ " contains top sort");