locale: print context for begin;
authorwenzelm
Thu Dec 14 15:31:20 2006 +0100 (2006-12-14 ago)
changeset 218432015be1b6a03
parent 21842 3d8ab6545049
child 21844 e10b8bd7a886
locale: print context for begin;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Dec 14 01:19:27 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 14 15:31:20 2006 +0100
     1.3 @@ -371,7 +371,7 @@
     1.4          -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
     1.5          -- P.opt_begin
     1.6        >> (fn (((is_open, name), (expr, elems)), begin) =>
     1.7 -          Toplevel.begin_local_theory begin
     1.8 +          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     1.9              (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin false)));
    1.10  
    1.11  val interpretationP =