src/Pure/old_goals.ML
changeset 29091 b81fe045e799
parent 27332 94790a9620c3
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/old_goals.ML	Fri Dec 12 22:13:13 2008 +0100
     1.2 +++ b/src/Pure/old_goals.ML	Sat Dec 13 15:00:39 2008 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  (*Generates the list of new theories when the proof state's theory changes*)
     1.6  fun thy_error (thy,thy') =
     1.7 -  let val names = Context.names_of thy' \\ Context.names_of thy
     1.8 +  let val names = Context.display_names thy' \\ Context.display_names thy
     1.9    in  case names of
    1.10          [name] => "\nNew theory: " ^ name
    1.11        | _       => "\nNew theories: " ^ space_implode ", " names