# HG changeset patch
# User wenzelm
# Date 1463256044 -7200
# Node ID 7910b1db2596c52c74730aa51b5d866e3200cf45
# Parent  201480e65b7d2a717bdb36d28c2f54c6a063051b
re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);

diff -r 201480e65b7d -r 7910b1db2596 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat May 14 19:59:43 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Sat May 14 22:00:44 2016 +0200
@@ -376,7 +376,9 @@
                   [((name, [Context_Rules.intro_query NONE]), asm)]) stmt;
           val that = Assumption.local_prems_of asms_ctxt stmt_ctxt;
           val ([(_, that')], that_ctxt) = asms_ctxt
-            |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])];
+            |> Proof_Context.set_stmt true
+            |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
+            ||> Proof_Context.restore_stmt asms_ctxt;
 
           val stmt' = [((Binding.empty, []), [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
         in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) end)