--- a/src/Pure/Isar/proof.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/Pure/Isar/proof.ML Fri Feb 23 20:55:46 2018 +0100
@@ -1059,8 +1059,8 @@
val ctxt'' =
ctxt'
|> not (null assumes_propss) ?
- (snd o Proof_Context.note_thmss ""
- [((Binding.name Auto_Bind.thatN, []), [(prems, [])])])
+ (snd o Proof_Context.note_thms ""
+ ((Binding.name Auto_Bind.thatN, []), [(prems, [])]))
|> (snd o Proof_Context.note_thmss ""
(assumes_bindings ~~ map (map (fn th => ([th], []))) premss))
in (prems, ctxt'') end);