# HG changeset patch
# User wenzelm
# Date 1427808549 -7200
# Node ID a04ea4709c8df61289a837a81077a3d71605113e
# Parent  8564d7abe5c5c30ef4633bd4f6e551bdbd951fe8
more standard Long_Name operations;

diff -r 8564d7abe5c5 -r a04ea4709c8d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 31 11:56:21 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 31 15:29:09 2015 +0200
@@ -396,9 +396,8 @@
 fun make_class clas = class_prefix ^ ascii_of clas
 
 fun new_skolem_var_name_of_const s =
-  let val ss = s |> space_explode Long_Name.separator in
-    nth ss (length ss - 2)
-  end
+  let val ss = Long_Name.explode s
+  in nth ss (length ss - 2) end
 
 (* These are ignored anyway by the relevance filter (unless they appear in
    higher-order places) but not by the monomorphizer. *)
diff -r 8564d7abe5c5 -r a04ea4709c8d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 31 11:56:21 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 31 15:29:09 2015 +0200
@@ -414,9 +414,8 @@
     val ps = map (`Long_Name.base_name) names;
     val dups = Library.duplicates (op =) (map fst ps);
     fun underscore s =
-      let val ss = space_explode Long_Name.separator s in
-        space_implode "_" (drop (length ss - 2) ss)
-      end;
+      let val ss = Long_Name.explode s
+      in space_implode "_" (drop (length ss - 2) ss) end;
   in
     map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
     |> Name.variant_list []
diff -r 8564d7abe5c5 -r a04ea4709c8d src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Tue Mar 31 11:56:21 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Tue Mar 31 15:29:09 2015 +0200
@@ -231,7 +231,7 @@
   | name_noted_thms qualifier base ((local_name, thms) :: noted) =
     if Long_Name.base_name local_name = base then
       (local_name,
-       map_index (uncurry (fn j => Thm.name_derivation (qualifier ^ Long_Name.separator ^ base ^
+       map_index (uncurry (fn j => Thm.name_derivation (Long_Name.append qualifier base ^
          (if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted
     else
       ((local_name, thms) :: name_noted_thms qualifier base noted);
diff -r 8564d7abe5c5 -r a04ea4709c8d src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 31 11:56:21 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 31 15:29:09 2015 +0200
@@ -66,8 +66,7 @@
         else metis_ad_hoc_type_tag, true))]
 
 fun old_skolem_const_name i j num_T_args =
-  old_skolem_const_prefix ^ Long_Name.separator ^
-  (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
+  Long_Name.implode (old_skolem_const_prefix :: map string_of_int [i, j, num_T_args])
 
 fun conceal_old_skolem_terms i old_skolems t =
   if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
diff -r 8564d7abe5c5 -r a04ea4709c8d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Mar 31 11:56:21 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Mar 31 15:29:09 2015 +0200
@@ -749,9 +749,7 @@
     let val hint = Thm.get_name_hint th in
       (* There must be a better way to detect local facts. *)
       (case try (unprefix local_prefix) hint of
-        SOME suf =>
-        thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
-        elided_backquote_thm 50 th
+        SOME suf => Long_Name.implode [thy_name_of_thm th, suf, elided_backquote_thm 50 th]
       | NONE => hint)
     end
   else
@@ -886,7 +884,7 @@
       | pattify_term _ _ (Free (s, T)) =
         maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
         |> (if member (op =) fixes s then
-              cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s)))
+              cons (free_feature_of (massage_long_name (Long_Name.append thy_name s)))
             else
               I)
       | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)