src/Pure/Isar/named_target.ML
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