Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
put_thms: do not index facts here (affects prems/this/calculation in particular);
authorwenzelm
Wed, 05 Mar 2008 21:24:06 +0100
changeset 26200 6bae051e8b7e
parent 26199 04817a8802f2
child 26201 d3363a854708
put_thms: do not index facts here (affects prems/this/calculation in particular);
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle