src/Pure/Isar/theory_target.ML
changeset 27690 24738db98d34
parent 27315 5d24085e0858
child 28083 103d9282a946
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Jul 29 08:15:38 2008 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Jul 29 08:15:39 2008 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  
     1.5  (* target declarations *)
     1.6  
     1.7 -fun target_decl add (Target {target, ...}) d lthy =
     1.8 +fun target_decl add (Target {target, is_class, ...}) d lthy =
     1.9    let
    1.10      val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
    1.11      val d0 = Morphism.form d';
    1.12 @@ -82,6 +82,7 @@
    1.13      else
    1.14        lthy
    1.15        |> LocalTheory.target (add target d')
    1.16 +      (*|> is_class ? LocalTheory.raw_theory (Class.declaration target d')*)
    1.17    end;
    1.18  
    1.19  val type_syntax = target_decl Locale.add_type_syntax;
    1.20 @@ -147,7 +148,7 @@
    1.21    |> ProofContext.note_thmss_i kind facts
    1.22    ||> ProofContext.restore_naming ctxt;
    1.23  
    1.24 -fun notes (Target {target, is_locale, ...}) kind facts lthy =
    1.25 +fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy =
    1.26    let
    1.27      val thy = ProofContext.theory_of lthy;
    1.28      val full = LocalTheory.full_name lthy;
    1.29 @@ -166,10 +167,9 @@
    1.30        (Sign.qualified_names
    1.31          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
    1.32          #> Sign.restore_naming thy)
    1.33 -
    1.34      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    1.35      |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    1.36 -
    1.37 +    (*|> is_class ? LocalTheory.raw_theory (Class.note target kind target_facts #> snd)*)
    1.38      |> note_local kind local_facts
    1.39    end;
    1.40