Theory.restore_naming;
tuned fold;

--- a/src/Pure/Proof/extraction.ML	Tue May 31 11:53:39 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue May 31 11:53:40 2005 +0200
@@ -746,9 +746,8 @@
 
     val defs = Library.foldl (fn (defs, (prf, vs)) =>
       fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
-    val {path, ...} = Sign.rep_sg sg;
 
-    fun add_def ((s, (vs, ((t, u), (prf, _)))), thy) =
+    fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
       (case Sign.const_type (sign_of thy) (extr_name s vs) of
          NONE =>
            let
@@ -768,10 +767,11 @@
            end
        | SOME _ => thy);
 
-  in thy |>
-    Theory.absolute_path |>
-    curry (Library.foldr add_def) defs |>
-    Theory.add_path (NameSpace.pack (getOpt (path,[])))
+  in
+    thy
+    |> Theory.absolute_path
+    |> fold_rev add_def defs
+    |> Theory.restore_naming thy
   end;