1.1 --- a/src/Pure/sign.ML	Sun Mar 18 13:04:22 2012 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Mar 18 13:37:11 2012 +0100
     1.3 @@ -204,8 +204,7 @@
     1.4  val naming_of = Name_Space.naming_of o Context.Theory;
     1.5  val map_naming = Context.theory_map o Name_Space.map_naming;
     1.6  val restore_naming = map_naming o K o naming_of;
     1.7 -fun inherit_naming thy =
     1.8 -  Context.Proof o Context.proof_map (Name_Space.map_naming (K (naming_of thy)));
     1.9 +fun inherit_naming thy = Name_Space.map_naming (K (naming_of thy)) o Context.Proof;
    1.10  
    1.11  val full_name = Name_Space.full_name o naming_of;
    1.12  fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));