1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Mar 21 11:06:39 2014 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Mar 21 11:42:32 2014 +0100
     1.3 @@ -85,8 +85,9 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
     1.8 -     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
     1.9 +  "term_of (f \<Colon> 'a \<Rightarrow> 'b) =
    1.10 +    Const (STR ''Pure.dummy_pattern'')
    1.11 +      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
    1.12  
    1.13  instance ..
    1.14  

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

     3.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 11:06:39 2014 +0100
     3.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 11:42:32 2014 +0100
     3.3 @@ -218,7 +218,7 @@
     3.4    (@{const_name induct_conj}, "'a"),*)
     3.5    (@{const_name "undefined"}, "'a"),
     3.6    (@{const_name "default"}, "'a"),
     3.7 -  (@{const_name "dummy_pattern"}, "'a::{}"),
     3.8 +  (@{const_name "Pure.dummy_pattern"}, "'a::{}"),
     3.9    (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
    3.10    (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
    3.11    (@{const_name "top_fun_inst.top_fun"}, "'a"),
    3.12 @@ -254,7 +254,7 @@
    3.13    "HOL.induct_forall",
    3.14   @{const_name undefined},
    3.15   @{const_name default},
    3.16 - @{const_name dummy_pattern},
    3.17 + @{const_name Pure.dummy_pattern},
    3.18   @{const_name "HOL.simp_implies"},
    3.19   @{const_name "bot_fun_inst.bot_fun"},
    3.20   @{const_name "top_fun_inst.top_fun"},

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

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

     6.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 11:06:39 2014 +0100
     6.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 11:42:32 2014 +0100
     6.3 @@ -127,8 +127,8 @@
     6.4              Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
     6.5        | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
     6.6            AbsP (s, case t of
     6.7 -                Const ("dummy_pattern", _) => NONE
     6.8 -              | _ $ Const ("dummy_pattern", _) => NONE
     6.9 +                Const ("Pure.dummy_pattern", _) => NONE
    6.10 +              | _ $ Const ("Pure.dummy_pattern", _) => NONE
    6.11                | _ => SOME (mk_term t),
    6.12              Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
    6.13        | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
    6.14 @@ -136,7 +136,7 @@
    6.15        | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
    6.16            prf_of (T::Ts) prf
    6.17        | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
    6.18 -          (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t))
    6.19 +          (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
    6.20        | prf_of _ t = error ("Not a proof term:\n" ^
    6.21            Syntax.string_of_term_global thy t)
    6.22  

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

     8.1 --- a/src/Pure/pure_thy.ML	Fri Mar 21 11:06:39 2014 +0100
     8.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 21 11:42:32 2014 +0100
     8.3 @@ -170,7 +170,7 @@
     8.4      ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
     8.5      ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
     8.6      (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
     8.7 -    (const "dummy_pattern", typ "aprop",               Delimfix "'_"),
     8.8 +    (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
     8.9      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
    8.10      (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
    8.11      (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
    8.12 @@ -200,12 +200,12 @@
    8.13      (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    8.14      (Binding.name "prop", typ "prop => prop", NoSyn),
    8.15      (Binding.name "TYPE", typ "'a itself", NoSyn),
    8.16 -    (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")]
    8.17 +    (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
    8.18    #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
    8.19    #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
    8.20    #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
    8.21    #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
    8.22 -  #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") []
    8.23 +  #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
    8.24    #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
    8.25    #> Sign.parse_translation Syntax_Trans.pure_parse_translation
    8.26    #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation

     9.1 --- a/src/Pure/term.ML	Fri Mar 21 11:06:39 2014 +0100
     9.2 +++ b/src/Pure/term.ML	Fri Mar 21 11:42:32 2014 +0100
     9.3 @@ -924,18 +924,18 @@
     9.4  
     9.5  (* dummy patterns *)
     9.6  
     9.7 -fun dummy_pattern T = Const ("dummy_pattern", T);
     9.8 +fun dummy_pattern T = Const ("Pure.dummy_pattern", T);
     9.9  val dummy = dummy_pattern dummyT;
    9.10  val dummy_prop = dummy_pattern propT;
    9.11  
    9.12 -fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
    9.13 +fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true
    9.14    | is_dummy_pattern _ = false;
    9.15  
    9.16  fun no_dummy_patterns tm =
    9.17    if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
    9.18    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
    9.19  
    9.20 -fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
    9.21 +fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used =
    9.22        let val [x] = Name.invent used Name.uu 1
    9.23        in (Free (Name.internal x, T), Name.declare x used) end
    9.24    | free_dummy_patterns (Abs (x, T, b)) used =
    9.25 @@ -948,7 +948,7 @@
    9.26        in (t' $ u', used'') end
    9.27    | free_dummy_patterns a used = (a, used);
    9.28  
    9.29 -fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
    9.30 +fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i =
    9.31        (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
    9.32    | replace_dummy Ts (Abs (x, T, t)) i =
    9.33        let val (t', i') = replace_dummy (T :: Ts) t i

    10.1 --- a/src/Tools/Code/code_thingol.ML	Fri Mar 21 11:06:39 2014 +0100
    10.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Mar 21 11:42:32 2014 +0100
    10.3 @@ -800,8 +800,8 @@
    10.4      val ty = fastype_of t;
    10.5      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
    10.6        o dest_TFree))) t [];
    10.7 -    val t' = annotate ctxt algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
    10.8 -    val dummy_constant = Constant @{const_name dummy_pattern};
    10.9 +    val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t;
   10.10 +    val dummy_constant = Constant @{const_name Pure.dummy_pattern};
   10.11      val stmt_value =
   10.12        fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs
   10.13        ##>> translate_typ ctxt algbr eqngr false ty
   10.14 @@ -818,7 +818,7 @@
   10.15          val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
   10.16        in ((program3, ((vs_ty, t), deps')), (deps, program2)) end;
   10.17    in
   10.18 -    ensure_stmt Constant stmt_value @{const_name dummy_pattern}
   10.19 +    ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern}
   10.20      #> snd
   10.21      #> term_value
   10.22    end;