--- a/src/Pure/Isar/element.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/element.ML Tue Jul 05 14:20:27 2016 +0200
@@ -492,7 +492,7 @@
let
val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
val asms = defs' |> map (fn (b, (t, ps)) =>
- let val (_, t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
+ let val (_, t') = Local_Defs.cert_def ctxt (K []) t (* FIXME adapt ps? *)
in (t', (b, [(t', ps)])) end);
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (map #1 asms)
@@ -517,7 +517,8 @@
(case (map_ctxt_attrib o map) Token.init_assignable elem of
Defines defs =>
Defines (defs |> map (fn ((a, atts), (t, ps)) =>
- ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
+ ((Thm.def_binding_optional
+ (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts),
(t, ps))))
| e => e);
val ctxt' = Context.proof_map (init elem') ctxt;