1.1 --- a/src/HOL/Import/proof_kernel.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4  fun smart_string_of_cterm ct =
     1.5      let
     1.6          val thy = Thm.theory_of_cterm ct
     1.7 -        val ctxt = ProofContext.init thy
     1.8 +        val ctxt = ProofContext.init_global thy
     1.9          val {t,T,...} = rep_cterm ct
    1.10          (* Hack to avoid parse errors with Trueprop *)
    1.11          val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)