src/Pure/Isar/theory_target.ML
changeset 28717 848ffc6b0b8a
parent 28707 548703affff5
child 28793 bb7a102e2f5d
equal deleted inserted replaced
28716:ee6f9e50f9c8 28717:848ffc6b0b8a
    82       |> LocalTheory.theory (Context.theory_map d0)
    82       |> LocalTheory.theory (Context.theory_map d0)
    83       |> LocalTheory.target (Context.proof_map d0)
    83       |> LocalTheory.target (Context.proof_map d0)
    84     else
    84     else
    85       lthy
    85       lthy
    86       |> LocalTheory.target (add target d')
    86       |> LocalTheory.target (add target d')
    87       (*|> is_class ? LocalTheory.raw_theory (Class.declaration target d')*)
       
    88   end;
    87   end;
    89 
    88 
    90 val type_syntax = target_decl Locale.add_type_syntax;
    89 val type_syntax = target_decl Locale.add_type_syntax;
    91 val term_syntax = target_decl Locale.add_term_syntax;
    90 val term_syntax = target_decl Locale.add_term_syntax;
    92 val declaration = target_decl Locale.add_declaration;
    91 val declaration = target_decl Locale.add_declaration;
   170       (Sign.qualified_names
   169       (Sign.qualified_names
   171         #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
   170         #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
   172         #> Sign.restore_naming thy)
   171         #> Sign.restore_naming thy)
   173     |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
   172     |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
   174     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
   173     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
   175     (*|> is_class ? LocalTheory.raw_theory (Class.note target kind target_facts #> snd)*)
       
   176     |> note_local kind local_facts
   174     |> note_local kind local_facts
   177   end;
   175   end;
   178 
   176 
   179 
   177 
   180 (* declare_const *)
   178 (* declare_const *)