re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
authorwenzelm
Sat May 14 22:00:44 2016 +0200 (2016-05-14 ago)
changeset 630967910b1db2596
parent 63095 201480e65b7d
child 63097 ee8edbcbb4ad
re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Sat May 14 19:59:43 2016 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Sat May 14 22:00:44 2016 +0200
     1.3 @@ -376,7 +376,9 @@
     1.4                    [((name, [Context_Rules.intro_query NONE]), asm)]) stmt;
     1.5            val that = Assumption.local_prems_of asms_ctxt stmt_ctxt;
     1.6            val ([(_, that')], that_ctxt) = asms_ctxt
     1.7 -            |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])];
     1.8 +            |> Proof_Context.set_stmt true
     1.9 +            |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
    1.10 +            ||> Proof_Context.restore_stmt asms_ctxt;
    1.11  
    1.12            val stmt' = [((Binding.empty, []), [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
    1.13          in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) end)