src/Pure/Isar/locale.ML
changeset 36653 8629ac3efb19
parent 36652 aace7a969410
parent 36610 bafd82950e24
child 36905 b47fd7148b57
     1.1 --- a/src/Pure/Isar/locale.ML	Tue May 04 19:57:55 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue May 04 20:30:22 2010 +0200
     1.3 @@ -309,7 +309,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  fun pretty_reg thy (name, morph) =
    1.14    let
    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;