src/Pure/Isar/locale.ML
changeset 36610 bafd82950e24
parent 36240 95a3fac5dcae
child 36653 8629ac3efb19
     1.1 --- a/src/Pure/Isar/locale.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -308,7 +308,7 @@
     1.4  
     1.5  fun init name thy =
     1.6    activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
     1.7 -    ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
     1.8 +    ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
     1.9  
    1.10  fun print_locale thy show_facts raw_name =
    1.11    let
    1.12 @@ -412,7 +412,7 @@
    1.13    let
    1.14      val name = intern thy raw_name;
    1.15      val name' = extern thy name;
    1.16 -    val ctxt = ProofContext.init thy;
    1.17 +    val ctxt = ProofContext.init_global thy;
    1.18      fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
    1.19      fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
    1.20      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;