src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Tue Jul 28 19:49:54 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 28 20:05:53 2015 +0200
@@ -501,7 +501,7 @@
       (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
         handle THM _ => err_lost ())
       |> Drule.flexflex_unique (SOME ctxt)
-      |> Thm.check_shyps (Variable.sorts_of ctxt)
+      |> Thm.check_shyps ctxt (Variable.sorts_of ctxt)
       |> Thm.check_hyps (Context.Proof ctxt);
 
     val goal_propss = filter_out null propss;