# HG changeset patch
# User wenzelm
# Date 1204748646 -3600
# Node ID 6bae051e8b7e23405a8f27cf55775a3943a52fd7
# Parent  04817a8802f296202bdb1eb4243f391341d2016f
put_thms: do not index facts here (affects prems/this/calculation in particular);

diff -r 04817a8802f2 -r 6bae051e8b7e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 05 21:24:03 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 05 21:24:06 2008 +0100
@@ -888,7 +888,7 @@
       in ((space', tab'), index') end);
 
 fun put_thms thms ctxt =
-  ctxt |> map_naming (K local_naming) |> update_thms (true, false) thms |> restore_naming ctxt;
+  ctxt |> map_naming (K local_naming) |> update_thms (false, false) thms |> restore_naming ctxt;
 
 
 (* note_thmss *)