# HG changeset patch
# User wenzelm
# Date 1256494769 -3600
# Node ID 853493e5d5d40a6b0005b2cb393092b87b72736a
# Parent  f02b804305d6caf37cfb36d5ebf261ee8dcc7c67
begin_theory: set theory_name here;

diff -r f02b804305d6 -r 853493e5d5d4 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Oct 25 19:18:59 2009 +0100
+++ b/src/Pure/theory.ML	Sun Oct 25 19:19:29 2009 +0100
@@ -141,7 +141,12 @@
   let
     val thy = Context.begin_thy Syntax.pp_global name imports;
     val wrappers = begin_wrappers thy;
-  in thy |> Sign.local_path |> apply_wrappers wrappers end;
+  in
+    thy
+    |> Sign.local_path
+    |> Sign.map_naming (Name_Space.set_theory_name name)
+    |> apply_wrappers wrappers
+  end;
 
 fun end_theory thy =
   thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;