--- a/src/HOL/Tools/inductive.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/inductive.ML Tue Jul 05 14:20:27 2016 +0200
@@ -1039,7 +1039,7 @@
let
val _ = Binding.is_empty name andalso null atts orelse
error "Abbreviations may not have names or attributes";
- val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t));
+ val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 (K []) t));
val var =
(case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
NONE => error ("Undeclared head of abbreviation " ^ quote x)