# HG changeset patch
# User wenzelm
# Date 1395263433 -3600
# Node ID 4c43a2881b2578736038d417239ce394360748c6
# Parent  bf80d125406b3078f8b66c8f9d0ae7dd50d4c695
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);

diff -r bf80d125406b -r 4c43a2881b25 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Mar 19 21:59:31 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Mar 19 22:10:33 2014 +0100
@@ -1309,7 +1309,7 @@
 fun mk_bind_eq prob_name params ((n, ty), t) =
   let
     val bnd =
-      Binding.name (List.last (space_explode "." n) ^ "_def")
+      Binding.name (Long_Name.base_name n ^ "_def")
       |> Binding.qualify false (TPTP_Problem_Name.mangle_problem_name prob_name)
     val t' =
       Term.list_comb (Const (n, ty), params)
diff -r bf80d125406b -r 4c43a2881b25 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Mar 19 21:59:31 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Mar 19 22:10:33 2014 +0100
@@ -722,7 +722,7 @@
 
     val bnd_def = (*FIXME consts*)
       const_name
-      |> space_implode "." o tl o space_explode "." (*FIXME hack to drop theory-name prefix*)
+      |> Long_Name.implode o tl o Long_Name.explode (*FIXME hack to drop theory-name prefix*)
       |> Binding.qualified_name
       |> Binding.suffix_name "_def"
 
diff -r bf80d125406b -r 4c43a2881b25 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 19 21:59:31 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 19 22:10:33 2014 +0100
@@ -444,7 +444,7 @@
 fun pretty_for_type ctxt = Syntax.pretty_typ ctxt o unarize_unbox_etc_type
 
 val prefix_name = Long_Name.qualify o Long_Name.base_name
-fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
+val shortest_name = Long_Name.base_name
 val prefix_abs_vars = Term.map_abs_vars o prefix_name
 
 fun short_name s =
diff -r bf80d125406b -r 4c43a2881b25 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 19 21:59:31 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 19 22:10:33 2014 +0100
@@ -148,7 +148,7 @@
 
 fun nth_atom thy atomss pool for_auto T j =
   if for_auto then
-    Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix))
+    Free (nth_atom_name thy atomss pool (hd (Long_Name.explode nitpick_prefix))
                         T j, T)
   else
     Const (nth_atom_name thy atomss pool "" T j, T)