1.1 --- a/src/Pure/goal.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/goal.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -211,7 +211,7 @@
     1.4  fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
     1.5  
     1.6  fun prove_global thy xs asms prop tac =
     1.7 -  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
     1.8 +  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
     1.9  
    1.10  
    1.11