1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 17 23:50:47 2012 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 17 23:55:03 2012 +0100
     1.3 @@ -141,6 +141,7 @@
     1.4      Context.generic -> Context.generic
     1.5    val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     1.6      Context.generic -> Context.generic
     1.7 +  val target_naming_of: Context.generic -> Name_Space.naming
     1.8    val class_alias: binding -> class -> Proof.context -> Proof.context
     1.9    val type_alias: binding -> string -> Proof.context -> Proof.context
    1.10    val const_alias: binding -> string -> Proof.context -> Proof.context
    1.11 @@ -992,6 +993,11 @@
    1.12  end;
    1.13  
    1.14  
    1.15 +(* naming *)
    1.16 +
    1.17 +val target_naming_of = Context.cases Sign.naming_of naming_of;
    1.18 +
    1.19 +
    1.20  (* aliases *)
    1.21  
    1.22  fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;

     2.1 --- a/src/Pure/simplifier.ML	Sat Mar 17 23:50:47 2012 +0100
     2.2 +++ b/src/Pure/simplifier.ML	Sat Mar 17 23:55:03 2012 +0100
     2.3 @@ -189,9 +189,8 @@
     2.4  
     2.5  fun gen_simproc prep {name = b, lhss, proc, identifier} lthy =
     2.6    let
     2.7 -    val naming = Local_Theory.naming_of lthy;
     2.8      val simproc = make_simproc
     2.9 -      {name = Name_Space.full_name naming b,
    2.10 +      {name = Local_Theory.full_name lthy b,
    2.11         lhss =
    2.12          let
    2.13            val lhss' = prep lthy lhss;
    2.14 @@ -201,8 +200,9 @@
    2.15         proc = proc,
    2.16         identifier = identifier};
    2.17    in
    2.18 -    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    2.19 +    lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
    2.20        let
    2.21 +        val naming = Proof_Context.target_naming_of context;
    2.22          val b' = Morphism.binding phi b;
    2.23          val simproc' = transform_simproc phi simproc;
    2.24        in