cleaned
authorhaftmann
Thu Nov 06 09:09:51 2008 +0100 (2008-11-06)
changeset 28717848ffc6b0b8a
parent 28716 ee6f9e50f9c8
child 28718 ef16499edaab
cleaned
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Nov 06 09:09:49 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Nov 06 09:09:51 2008 +0100
     1.3 @@ -84,7 +84,6 @@
     1.4      else
     1.5        lthy
     1.6        |> LocalTheory.target (add target d')
     1.7 -      (*|> is_class ? LocalTheory.raw_theory (Class.declaration target d')*)
     1.8    end;
     1.9  
    1.10  val type_syntax = target_decl Locale.add_type_syntax;
    1.11 @@ -172,7 +171,6 @@
    1.12          #> Sign.restore_naming thy)
    1.13      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    1.14      |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    1.15 -    (*|> is_class ? LocalTheory.raw_theory (Class.note target kind target_facts #> snd)*)
    1.16      |> note_local kind local_facts
    1.17    end;
    1.18