# HG changeset patch
# User ballarin
# Date 1126879642 -7200
# Node ID e40afa46107877e3d75656f5c5b7e5e8a0a41640
# Parent  9deaf32c83bec13f3b147bd011c5e984b10faa36
tuned

diff -r 9deaf32c83be -r e40afa461078 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Sep 16 14:46:31 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Sep 16 16:07:22 2005 +0200
@@ -2412,13 +2412,9 @@
 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
   map (rpair ([], [])) props);
 
-fun prop_name thy propss =
-    propss |> map (fn ((name, _), _) => extern thy name);
-fun goal_name thy kind NONE propss =
-    kind ^ (Proof.goal_names NONE "" (prop_name thy propss))
-  | goal_name thy kind (SOME target) propss =
-    kind ^ (Proof.goal_names (SOME (extern thy target)) ""
-      (prop_name thy propss));
+fun goal_name thy kind target propss =
+    kind ^ Proof.goal_names (Option.map (extern thy) target) ""
+      (propss |> map (fn ((name, _), _) => extern thy name));
 
 in