src/Pure/Isar/proof_context.ML
changeset 26200 6bae051e8b7e
parent 25476 03da46cfab9e
child 26240 cc630a75b62a
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 05 21:24:03 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 05 21:24:06 2008 +0100
     1.3 @@ -888,7 +888,7 @@
     1.4        in ((space', tab'), index') end);
     1.5  
     1.6  fun put_thms thms ctxt =
     1.7 -  ctxt |> map_naming (K local_naming) |> update_thms (true, false) thms |> restore_naming ctxt;
     1.8 +  ctxt |> map_naming (K local_naming) |> update_thms (false, false) thms |> restore_naming ctxt;
     1.9  
    1.10  
    1.11  (* note_thmss *)