src/Pure/Isar/isar_cmd.ML
changeset 15624 484178635bd8
parent 15596 8665d08085df
child 15703 727ef1b8b3ee
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 24 16:36:40 2005 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 24 17:03:37 2005 +0100
     1.3 @@ -222,10 +222,9 @@
     1.4      Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body)
     1.5    end);
     1.6  
     1.7 -fun print_registrations name = Toplevel.unknown_theory o
     1.8 -  Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in
     1.9 -    Locale.print_global_registrations thy name
    1.10 -  end);
    1.11 +fun print_registrations name = Toplevel.unknown_context o
    1.12 +  Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations name)
    1.13 +    (Locale.print_local_registrations name o Proof.context_of));
    1.14  
    1.15  val print_attributes = Toplevel.unknown_theory o
    1.16    Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);