# HG changeset patch
# User wenzelm
# Date 1330358185 -3600
# Node ID f745bcc4a1e555c98a5c57a3593ea76e2d394b08
# Parent  cb9168bf3cf77531bf5d89622f2faa781fd7ff2e
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);

diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/HOL/Mutabelle/Mutabelle.thy
--- a/src/HOL/Mutabelle/Mutabelle.thy	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Mutabelle/Mutabelle.thy	Mon Feb 27 16:56:25 2012 +0100
@@ -1,3 +1,5 @@
+(* FIXME dead code!?!? *)
+
 theory Mutabelle
 imports Main
 uses "mutabelle.ML"
@@ -26,7 +28,7 @@
  [@{const_name nibble_pair_of_char}];
 
 fun is_forbidden s th =
- exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
+ exists (fn s' => s' mem Long_Name.explode s) forbidden_thms orelse
  exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts;
 
 fun test j = List.app (fn i =>
diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Feb 27 16:56:25 2012 +0100
@@ -235,13 +235,13 @@
 
 fun is_forbidden_theorem (s, th) =
   let val consts = Term.add_const_names (prop_of th) [] in
-    exists (member (op =) (space_explode "." s)) forbidden_thms orelse
+    exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
     exists (member (op =) forbidden_consts) consts orelse
-    length (space_explode "." s) <> 2 orelse
-    String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
+    length (Long_Name.explode s) <> 2 orelse
+    String.isPrefix "type_definition" (List.last (Long_Name.explode s)) orelse
     String.isSuffix "_def" s orelse
     String.isSuffix "_raw" s orelse
-    String.isPrefix "term_of" (List.last (space_explode "." s))
+    String.isPrefix "term_of" (List.last (Long_Name.explode s))
   end
 
 val forbidden_mutant_constnames =
diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 27 16:56:25 2012 +0100
@@ -154,9 +154,9 @@
   end
 
 fun is_forbidden_theorem name =
-  length (space_explode "." name) <> 2 orelse
-  String.isPrefix "type_definition" (List.last (space_explode "." name)) orelse
-  String.isPrefix "arity_" (List.last (space_explode "." name)) orelse
+  length (Long_Name.explode name) <> 2 orelse
+  String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
+  String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
   String.isSuffix "_def" name orelse
   String.isSuffix "_raw" name
 
diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Feb 27 16:56:25 2012 +0100
@@ -493,7 +493,7 @@
 
 fun new_skolem_const_name s num_T_args =
   [new_skolem_const_prefix, s, string_of_int num_T_args]
-  |> space_implode Long_Name.separator
+  |> Long_Name.implode
 
 fun robust_const_type thy s =
   if s = app_op_name then
diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Feb 27 16:56:25 2012 +0100
@@ -360,7 +360,7 @@
    constant name. *)
 fun num_type_args thy s =
   if String.isPrefix skolem_const_prefix s then
-    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
+    s |> Long_Name.explode |> List.last |> Int.fromString |> the
   else if String.isPrefix lam_lifted_prefix s then
     if String.isPrefix lam_lifted_poly_prefix s then 2 else 0
   else
diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Feb 27 16:56:25 2012 +0100
@@ -102,7 +102,7 @@
 
 val unyxml = XML.content_of o YXML.parse_body
 
-val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
+val is_long_identifier = forall Lexicon.is_identifier o Long_Name.explode
 fun maybe_quote y =
   let val s = unyxml y in
     y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Feb 27 16:56:25 2012 +0100
@@ -94,7 +94,7 @@
 exception NOT_SUPPORTED of string
 exception SAME of unit
 
-val nitpick_prefix = "Nitpick."
+val nitpick_prefix = "Nitpick" ^ Long_Name.separator
 
 fun curry3 f = fn x => fn y => fn z => f (x, y, z)
 
diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 16:56:25 2012 +0100
@@ -41,7 +41,7 @@
     val ctxt' = ctxt
        |> Config.put Quickcheck.abort_potential true
        |> Config.put Quickcheck.quiet true
-    val all_thms = filter (fn (s, _) => length (space_explode "." s) = 2)
+    val all_thms = filter (fn (s, _) => length (Long_Name.explode s) = 2)  (* FIXME !? *)
       (thms_of (Proof_Context.theory_of ctxt) thy_name)
     fun check_single conjecture =
       case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
diff -r cb9168bf3cf7 -r f745bcc4a1e5 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Feb 27 16:56:25 2012 +0100
@@ -642,7 +642,7 @@
         fun splitthy id =
             let val comps = Long_Name.explode id
             in case comps of
-                   (thy::(rest as _::_)) => (Thy_Info.get_theory thy, space_implode "." rest)
+                   (thy::(rest as _::_)) => (Thy_Info.get_theory thy, Long_Name.implode rest)
                  | [plainid] => (topthy(),plainid)
                  | _ => raise Toplevel.UNDEF (* assert false *)
             end