src/Pure/Isar/isar_cmd.ML
changeset 29223 e09c53289830
parent 29006 abe0f11cfa4e
child 29230 155f6c110dfc
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -53,8 +53,7 @@
     1.4    val print_configs: Toplevel.transition -> Toplevel.transition
     1.5    val print_theorems: Toplevel.transition -> Toplevel.transition
     1.6    val print_locales: Toplevel.transition -> Toplevel.transition
     1.7 -  val print_locale: bool * (Locale.expr * Element.context list)
     1.8 -    -> Toplevel.transition -> Toplevel.transition
     1.9 +  val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
    1.10    val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
    1.11    val print_attributes: Toplevel.transition -> Toplevel.transition
    1.12    val print_simpset: Toplevel.transition -> Toplevel.transition
    1.13 @@ -354,11 +353,11 @@
    1.14  val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
    1.15  
    1.16  val print_locales = Toplevel.unknown_theory o
    1.17 -  Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
    1.18 +  Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of);
    1.19  
    1.20 -fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o
    1.21 +fun print_locale (show_facts, name) = Toplevel.unknown_theory o
    1.22    Toplevel.keep (fn state =>
    1.23 -    Locale.print_locale (Toplevel.theory_of state) show_facts imports body);
    1.24 +    NewLocale.print_locale (Toplevel.theory_of state) show_facts name);
    1.25  
    1.26  fun print_registrations show_wits name = Toplevel.unknown_context o
    1.27    Toplevel.keep (Toplevel.node_case