# HG changeset patch # User haftmann # Date 1225958991 -3600 # Node ID 848ffc6b0b8a0b08cc71274a888b21c6b1615149 # Parent ee6f9e50f9c8a891de56f31e3f239bb52b1c9a3a cleaned diff -r ee6f9e50f9c8 -r 848ffc6b0b8a src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Thu Nov 06 09:09:49 2008 +0100 +++ b/src/Pure/Isar/theory_target.ML Thu Nov 06 09:09:51 2008 +0100 @@ -84,7 +84,6 @@ else lthy |> LocalTheory.target (add target d') - (*|> is_class ? LocalTheory.raw_theory (Class.declaration target d')*) end; val type_syntax = target_decl Locale.add_type_syntax; @@ -172,7 +171,6 @@ #> Sign.restore_naming thy) |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd) |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts) - (*|> is_class ? LocalTheory.raw_theory (Class.note target kind target_facts #> snd)*) |> note_local kind local_facts end;