Context.display_names;
authorwenzelm
Sat Dec 13 15:00:39 2008 +0100 (2008-12-13)
changeset 29091b81fe045e799
parent 29090 bbfac5fd8d78
child 29092 466a83cb6f5f
Context.display_names;
src/Pure/display.ML
src/Pure/old_goals.ML
     1.1 --- a/src/Pure/display.ML	Fri Dec 12 22:13:13 2008 +0100
     1.2 +++ b/src/Pure/display.ML	Sat Dec 13 15:00:39 2008 +0100
     1.3 @@ -213,7 +213,7 @@
     1.4        ||> List.partition (Defs.plain_args o #2 o #1);
     1.5      val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
     1.6    in
     1.7 -    [Pretty.strs ("names:" :: Context.names_of thy)] @
     1.8 +    [Pretty.strs ("names:" :: Context.display_names thy)] @
     1.9      [Pretty.strs ["name prefix:", NameSpace.path_of naming],
    1.10        Pretty.big_list "classes:" (map pretty_classrel clsses),
    1.11        pretty_default default,
     2.1 --- a/src/Pure/old_goals.ML	Fri Dec 12 22:13:13 2008 +0100
     2.2 +++ b/src/Pure/old_goals.ML	Sat Dec 13 15:00:39 2008 +0100
     2.3 @@ -127,7 +127,7 @@
     2.4  
     2.5  (*Generates the list of new theories when the proof state's theory changes*)
     2.6  fun thy_error (thy,thy') =
     2.7 -  let val names = Context.names_of thy' \\ Context.names_of thy
     2.8 +  let val names = Context.display_names thy' \\ Context.display_names thy
     2.9    in  case names of
    2.10          [name] => "\nNew theory: " ^ name
    2.11        | _       => "\nNew theories: " ^ space_implode ", " names