--- a/src/Pure/Isar/obtain.ML Sat Jun 13 17:14:05 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Sat Jun 13 19:38:26 2015 +0200
@@ -151,12 +151,13 @@
val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt;
val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
+ val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains;
in
state
|> Proof.have NONE (K I)
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
(map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
- [((Binding.empty, obtains_attributes raw_obtains), [(thesis, [])])] int
+ [((Binding.empty, atts), [(thesis, [])])] int
|> (fn state' => state'
|> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
end;