1.1 --- a/src/Pure/Isar/local_theory.ML	Sat Oct 29 12:55:34 2011 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Oct 29 12:57:43 2011 +0200
     1.3 @@ -231,8 +231,7 @@
     1.4  fun alias global_alias local_alias b name =
     1.5    declaration {syntax = true, pervasive = false} (fn phi =>
     1.6      let val b' = Morphism.binding phi b
     1.7 -    in Context.mapping (global_alias b' name) (local_alias b' name) end)
     1.8 -  #> local_alias b name;
     1.9 +    in Context.mapping (global_alias b' name) (local_alias b' name) end);
    1.10  
    1.11  val class_alias = alias Sign.class_alias Proof_Context.class_alias;
    1.12  val type_alias = alias Sign.type_alias Proof_Context.type_alias;