# HG changeset patch
# User wenzelm
# Date 1117533220 -7200
# Node ID d8cac577493c3d739c1bacbb4570b6c34b4fc996
# Parent  5f15a14122dce597e7eb1b44ef4653d387120962
Theory.restore_naming;
tuned fold;

diff -r 5f15a14122dc -r d8cac577493c src/Pure/Proof/extraction.ML
--- 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;