# HG changeset patch
# User wenzelm
# Date 1467636679 -7200
# Node ID a4d0dc3ea28fef7ef9a58b361bb99556c6b4fe87
# Parent  4698dd1106aebee91d9fc0cd1a93455cdc01cc84
more accurate facts index;

diff -r 4698dd1106ae -r a4d0dc3ea28f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jul 04 11:11:19 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jul 04 14:51:19 2016 +0200
@@ -255,12 +255,12 @@
     [thm] => thm
   | _ => error "Single theorem expected");
 
-fun put_facts facts =
+fun put_facts index facts =
   map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
-  map_context (Proof_Context.put_thms true (Auto_Bind.thisN, facts));
+  map_context (Proof_Context.put_thms index (Auto_Bind.thisN, facts));
 
-val set_facts = put_facts o SOME;
-val reset_facts = put_facts NONE;
+val set_facts = put_facts false o SOME;
+val reset_facts = put_facts false NONE;
 
 fun these_factss more_facts (named_factss, state) =
   (named_factss, state |> set_facts (maps snd named_factss @ more_facts));
@@ -271,7 +271,7 @@
   | SOME thms =>
       thms
       |> Proof_Context.export (context_of inner) (context_of outer)
-      |> (fn ths => set_facts ths outer));
+      |> (fn ths => put_facts true (SOME ths) outer));
 
 
 (* mode *)