src/Pure/Proof/extraction.ML
changeset 48704 85a3de10567d
parent 48646 91281e9472d8
child 49960 1167c1157a5b
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Aug 07 10:28:04 2012 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Aug 07 12:10:26 2012 +0200
     1.3 @@ -120,7 +120,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 (Symbol.spaces d ^ s);
     1.8 +fun msg d s = Output.urgent_message (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 []));