diff -r 7faeff3156d5 -r 734723445a8c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -330,7 +330,7 @@
           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
-            let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
+            let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t)
             in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
         | e => e)
       end;
@@ -540,7 +540,7 @@
 
 fun bind_def ctxt eq (xs, env, eqs) =
   let
-    val _ = Local_Defs.cert_def ctxt eq;
+    val _ = Local_Defs.cert_def ctxt (K []) eq;
     val ((y, T), b) = Local_Defs.abs_def eq;
     val b' = norm_term env b;
     fun err msg = error (msg ^ ": " ^ quote y);