--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Apr 28 09:43:11 2016 +0200
@@ -623,12 +623,12 @@
else if Binding.eq_name (b, equal_binding) then
pair (Term.lambda u exist_xs_u_eq_ctr, refl)
else
- Specification.definition (SOME (b, NONE, NoSyn),
- ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
+ Specification.definition (SOME (b, NONE, NoSyn)) []
+ ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd)
ks exist_xs_u_eq_ctrs disc_bindings
||>> apfst split_list o fold_map (fn (b, proto_sels) =>
- Specification.definition (SOME (b, NONE, NoSyn),
- ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
+ Specification.definition (SOME (b, NONE, NoSyn)) []
+ ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy lthy';