--- a/src/Pure/Isar/method.ML Thu Aug 14 12:13:24 2014 +0200
+++ b/src/Pure/Isar/method.ML Thu Aug 14 12:33:21 2014 +0200
@@ -356,11 +356,7 @@
|> Local_Theory.background_theory_result (define_global binding meth0 comment)
|-> (fn name =>
Local_Theory.map_contexts (K transfer_methods)
- #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
- let
- val naming = Name_Space.naming_of context;
- val binding' = Morphism.binding phi binding;
- in Methods.map (Name_Space.alias_table naming binding' name) context end)
+ #> Local_Theory.generic_alias Methods.map binding name
#> pair name)
end;