src/Pure/Proof/extraction.ML
changeset 58843 521cea5fa777
parent 58436 fe9de4089345
child 58950 d07464875dd4
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Oct 31 11:18:17 2014 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Oct 31 11:36:41 2014 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4  fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
     1.5  fun corr_name s vs = extr_name s vs ^ "_correctness";
     1.6  
     1.7 -fun msg d s = Output.urgent_message (Pretty.spaces d ^ s);
     1.8 +fun msg d s = writeln (Pretty.spaces d ^ s);
     1.9  
    1.10  fun vars_of t = map Var (rev (Term.add_vars t []));
    1.11  fun frees_of t = map Free (rev (Term.add_frees t []));