Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
authorballarin
Tue Oct 28 17:53:46 2008 +0100 (2008-10-28)
changeset 28707548703affff5
parent 28706 3fef773ae6b1
child 28708 a1a436f09ec6
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Oct 28 16:59:02 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Oct 28 17:53:46 2008 +0100
     1.3 @@ -186,7 +186,7 @@
     1.4  
     1.5  fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
     1.6    let
     1.7 -    val c' = Morphism.name phi c |> Name.map_name NameSpace.base;  (* FIXME !!! *)
     1.8 +    val c' = Morphism.name phi c;
     1.9      val rhs' = Morphism.term phi rhs;
    1.10      val name = Name.name_of c;
    1.11      val name' = Name.name_of c';