more qualified names;

--- a/src/HOL/Code_Evaluation.thy	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Mar 21 11:42:32 2014 +0100
@@ -85,8 +85,9 @@
 begin
 
 definition
-  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
-     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
+  "term_of (f \<Colon> 'a \<Rightarrow> 'b) =
+    Const (STR ''Pure.dummy_pattern'')
+      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
 
 instance ..
 

--- a/src/HOL/List.thy	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/HOL/List.thy	Fri Mar 21 11:42:32 2014 +0100
@@ -439,7 +439,7 @@
         val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
         val case2 =
           Syntax.const @{syntax_const "_case1"} $
-            Syntax.const @{const_syntax dummy_pattern} $ NilC;
+            Syntax.const @{const_syntax Pure.dummy_pattern} $ NilC;
         val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
       in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end;
 

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 11:42:32 2014 +0100
@@ -218,7 +218,7 @@
   (@{const_name induct_conj}, "'a"),*)
   (@{const_name "undefined"}, "'a"),
   (@{const_name "default"}, "'a"),
-  (@{const_name "dummy_pattern"}, "'a::{}"),
+  (@{const_name "Pure.dummy_pattern"}, "'a::{}"),
   (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
   (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
   (@{const_name "top_fun_inst.top_fun"}, "'a"),
@@ -254,7 +254,7 @@
   "HOL.induct_forall",
  @{const_name undefined},
  @{const_name default},
- @{const_name dummy_pattern},
+ @{const_name Pure.dummy_pattern},
  @{const_name "HOL.simp_implies"},
  @{const_name "bot_fun_inst.bot_fun"},
  @{const_name "top_fun_inst.top_fun"},

--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 21 11:42:32 2014 +0100
@@ -149,7 +149,7 @@
           | abs_pat _ _ = I;
 
         (* replace occurrences of dummy_pattern by distinct variables *)
-        fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used =
+        fun replace_dummies (Const (@{const_syntax Pure.dummy_pattern}, T)) used =
               let val (x, used') = variant_free "x" used
               in (Free (x, T), used') end
           | replace_dummies (t $ u) used =

--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 21 11:42:32 2014 +0100
@@ -428,7 +428,7 @@
 fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = 
   let
     val frees = Term.add_free_names t []
-    val dummy_term = @{term "Code_Evaluation.Const (STR ''dummy_pattern'')
+    val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'')
       (Typerep.Typerep (STR ''dummy'') [])"}
     val return = @{term "Some :: term list => term list option"} $
       (HOLogic.mk_list @{typ "term"}

--- a/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 11:42:32 2014 +0100
@@ -127,8 +127,8 @@
             Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
       | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
           AbsP (s, case t of
-                Const ("dummy_pattern", _) => NONE
-              | _ $ Const ("dummy_pattern", _) => NONE
+                Const ("Pure.dummy_pattern", _) => NONE
+              | _ $ Const ("Pure.dummy_pattern", _) => NONE
               | _ => SOME (mk_term t),
             Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
       | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
@@ -136,7 +136,7 @@
       | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
           prf_of (T::Ts) prf
       | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
-          (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t))
+          (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
       | prf_of _ t = error ("Not a proof term:\n" ^
           Syntax.string_of_term_global thy t)
 

--- a/src/Pure/Syntax/syntax_phases.ML	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Mar 21 11:42:32 2014 +0100
@@ -177,7 +177,7 @@
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
-      | asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) =
+      | asts_of (Parser.Node (a as "\\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
           [ast_of_dummy a tok]
       | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
           [ast_of_dummy a tok]

--- a/src/Pure/pure_thy.ML	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/Pure/pure_thy.ML	Fri Mar 21 11:42:32 2014 +0100
@@ -170,7 +170,7 @@
     ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
     ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
     (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
-    (const "dummy_pattern", typ "aprop",               Delimfix "'_"),
+    (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
     (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
     (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
@@ -200,12 +200,12 @@
     (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
     (Binding.name "prop", typ "prop => prop", NoSyn),
     (Binding.name "TYPE", typ "'a itself", NoSyn),
-    (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")]
+    (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
   #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
   #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
   #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
   #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
-  #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") []
+  #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation

--- a/src/Pure/term.ML	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/Pure/term.ML	Fri Mar 21 11:42:32 2014 +0100
@@ -924,18 +924,18 @@
 
 (* dummy patterns *)
 
-fun dummy_pattern T = Const ("dummy_pattern", T);
+fun dummy_pattern T = Const ("Pure.dummy_pattern", T);
 val dummy = dummy_pattern dummyT;
 val dummy_prop = dummy_pattern propT;
 
-fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
+fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true
   | is_dummy_pattern _ = false;
 
 fun no_dummy_patterns tm =
   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
 
-fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
+fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used =
       let val [x] = Name.invent used Name.uu 1
       in (Free (Name.internal x, T), Name.declare x used) end
   | free_dummy_patterns (Abs (x, T, b)) used =
@@ -948,7 +948,7 @@
       in (t' $ u', used'') end
   | free_dummy_patterns a used = (a, used);
 
-fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
+fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i =
       (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
   | replace_dummy Ts (Abs (x, T, t)) i =
       let val (t', i') = replace_dummy (T :: Ts) t i

--- a/src/Tools/Code/code_thingol.ML	Fri Mar 21 11:06:39 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Fri Mar 21 11:42:32 2014 +0100
@@ -800,8 +800,8 @@
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
-    val t' = annotate ctxt algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
-    val dummy_constant = Constant @{const_name dummy_pattern};
+    val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t;
+    val dummy_constant = Constant @{const_name Pure.dummy_pattern};
     val stmt_value =
       fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs
       ##>> translate_typ ctxt algbr eqngr false ty
@@ -818,7 +818,7 @@
         val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
       in ((program3, ((vs_ty, t), deps')), (deps, program2)) end;
   in
-    ensure_stmt Constant stmt_value @{const_name dummy_pattern}
+    ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern}
     #> snd
     #> term_value
   end;