# HG changeset patch
# User ballarin
# Date 1225120852 -3600
# Node ID f1701105d6511506b859149bb78f4cc4123d0857
# Parent  f7a06d7284c8f03fa5c0659d7f06242bc0bcd3cf
Hide path in constant name (workaround).

diff -r f7a06d7284c8 -r f1701105d651 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Oct 27 16:15:50 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Oct 27 16:20:52 2008 +0100
@@ -186,7 +186,7 @@
 
 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
   let
-    val c' = Morphism.name phi c;
+    val c' = Morphism.name phi c |> Name.map_name NameSpace.base;  (* FIXME !!! *)
     val rhs' = Morphism.term phi rhs;
     val name = Name.name_of c;
     val name' = Name.name_of c';