| changeset 40132 | 7ee65dbffa31 |
| parent 39557 | fe5722fce758 |
| child 40627 | becf5d5187cc |
--- a/src/Pure/Proof/extraction.ML Mon Oct 25 20:24:13 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Mon Oct 25 21:06:56 2010 +0200 @@ -119,7 +119,7 @@ fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs)); fun corr_name s vs = extr_name s vs ^ "_correctness"; -fun msg d s = priority (Symbol.spaces d ^ s); +fun msg d s = Output.urgent_message (Symbol.spaces d ^ s); fun vars_of t = map Var (rev (Term.add_vars t [])); fun frees_of t = map Free (rev (Term.add_frees t []));