--- 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;