equal
deleted
inserted
replaced
125 |
125 |
126 (*** Setting up goal-directed proof ***) |
126 (*** Setting up goal-directed proof ***) |
127 |
127 |
128 (*Generates the list of new theories when the proof state's theory changes*) |
128 (*Generates the list of new theories when the proof state's theory changes*) |
129 fun thy_error (thy,thy') = |
129 fun thy_error (thy,thy') = |
130 let val names = Context.names_of thy' \\ Context.names_of thy |
130 let val names = Context.display_names thy' \\ Context.display_names thy |
131 in case names of |
131 in case names of |
132 [name] => "\nNew theory: " ^ name |
132 [name] => "\nNew theory: " ^ name |
133 | _ => "\nNew theories: " ^ space_implode ", " names |
133 | _ => "\nNew theories: " ^ space_implode ", " names |
134 end; |
134 end; |
135 |
135 |