src/Pure/Isar/proof_display.ML
changeset 36610 bafd82950e24
parent 33643 b275f26a638b
child 39284 3aefd3342978
     1.1 --- a/src/Pure/Isar/proof_display.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  fun pretty_theorems_diff verbose prev_thys thy =
     1.6    let
     1.7 -    val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
     1.8 +    val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy);
     1.9      val facts = PureThy.facts_of thy;
    1.10      val thmss =
    1.11        Facts.dest_static (map PureThy.facts_of prev_thys) facts