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