changeset 59876 | 8564d7abe5c5 |
parent 58665 | 50b229a5a097 |
child 59880 | 30687c3f2b10 |
--- a/src/Pure/Isar/named_target.ML Tue Mar 31 11:39:24 2015 +0200 +++ b/src/Pure/Isar/named_target.ML Tue Mar 31 11:56:21 2015 +0200 @@ -155,8 +155,8 @@ fun gen_init before_exit target thy = let val name_data = make_name_data thy target; - val naming = Sign.naming_of thy - |> Name_Space.mandatory_path (Long_Name.base_name target); + val naming = + Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target); in thy |> Sign.change_begin