--- a/src/Pure/Isar/locale.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/locale.ML Mon May 03 14:25:56 2010 +0200
@@ -308,7 +308,7 @@
fun init name thy =
activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
- ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
+ ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
fun print_locale thy show_facts raw_name =
let
@@ -412,7 +412,7 @@
let
val name = intern thy raw_name;
val name' = extern thy name;
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;