src/Pure/Proof/extraction.ML
changeset 30364 577edc39b501
parent 30344 10a67c5ddddb
child 30435 e62d6ecab6ad
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -119,7 +119,7 @@
     1.4  
     1.5  val chtype = change_type o SOME;
     1.6  
     1.7 -fun extr_name s vs = NameSpace.append "extr" (space_implode "_" (s :: vs));
     1.8 +fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
     1.9  fun corr_name s vs = extr_name s vs ^ "_correctness";
    1.10  
    1.11  fun msg d s = priority (Symbol.spaces d ^ s);