src/Pure/Isar/theory_target.ML
changeset 25684 2b3cce7d22b8
parent 25607 779c79c36c5e
child 25864 11f531354852
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Dec 17 22:40:13 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Dec 17 22:40:14 2007 +0100
     1.3 @@ -144,6 +144,12 @@
     1.4  
     1.5    in (result'', result) end;
     1.6  
     1.7 +fun note_local kind facts ctxt =
     1.8 +  ctxt
     1.9 +  |> ProofContext.qualified_names
    1.10 +  |> ProofContext.note_thmss_i kind facts
    1.11 +  ||> ProofContext.restore_naming ctxt;
    1.12 +
    1.13  fun notes (Target {target, is_locale, ...}) kind facts lthy =
    1.14    let
    1.15      val thy = ProofContext.theory_of lthy;
    1.16 @@ -164,11 +170,10 @@
    1.17          #> PureThy.note_thmss_i kind global_facts #> snd
    1.18          #> Sign.restore_naming thy)
    1.19  
    1.20 +    |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    1.21      |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    1.22  
    1.23 -    |> ProofContext.qualified_names
    1.24 -    |> ProofContext.note_thmss_i kind local_facts
    1.25 -    ||> ProofContext.restore_naming lthy
    1.26 +    |> note_local kind local_facts
    1.27    end;
    1.28  
    1.29