added Term.dummy_pattern conveniences;

--- a/src/HOL/Tools/Datatype/datatype_case.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -346,7 +346,7 @@
                   (fold_rev count_cases cases []);
                 val R = type_of t;
                 val dummy =
-                  if d then Const (@{const_name dummy_pattern}, R)
+                  if d then Term.dummy_pattern R
                   else Free (singleton (Name.variant_list used) "x", R);
               in
                 SOME (x,

--- a/src/HOL/Tools/Function/function_lib.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -75,9 +75,7 @@
   let
     val allthm = Thm.forall_intr cv thm
     val (_ $ abs) = prop_of allthm
-  in
-    Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
-  end
+  in Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy)) allthm end
 
 
 datatype proof_attempt = Solved of thm | Stuck of thm | Fail

--- a/src/Pure/Proof/proof_syntax.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -172,12 +172,12 @@
         Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
       end
   | term_of Ts (AbsP (s, t, prf)) =
-      AbsPt $ the_default (Term.dummy_pattern propT) t $
+      AbsPt $ the_default Term.dummy_prop t $
         Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
   | term_of Ts (prf1 %% prf2) =
       AppPt $ term_of Ts prf1 $ term_of Ts prf2
   | term_of Ts (prf % opt) =
-      let val t = the_default (Term.dummy_pattern dummyT) opt
+      let val t = the_default Term.dummy opt
       in Const ("Appt",
         [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
           term_of Ts prf $ t

--- a/src/Pure/drule.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/Pure/drule.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -729,7 +729,7 @@
 fun cterm_rule f = dest_term o f o mk_term;
 fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));
 
-val dummy_thm = mk_term (certify (Term.dummy_pattern propT));
+val dummy_thm = mk_term (certify Term.dummy_prop);
 
 
 (* sort_constraint *)

--- a/src/Pure/proofterm.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/Pure/proofterm.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -1051,10 +1051,8 @@
 
 val axm_proof = gen_axm_proof PAxm;
 
-val dummy = Const (Term.dummy_patternN, dummyT);
-
 fun oracle_proof name prop =
-  if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
+  if ! proofs = 0 then ((name, Term.dummy), Oracle (name, Term.dummy, NONE))
   else ((name, prop), gen_axm_proof Oracle name prop);
 
 fun shrink_proof thy =

--- a/src/Pure/term.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/Pure/term.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -164,6 +164,8 @@
   val dest_abs: string * typ * term -> string * term
   val dummy_patternN: string
   val dummy_pattern: typ -> term
+  val dummy: term
+  val dummy_prop: term
   val is_dummy_pattern: term -> bool
   val free_dummy_patterns: term -> Name.context -> term * Name.context
   val no_dummy_patterns: term -> term
@@ -941,6 +943,8 @@
 val dummy_patternN = "dummy_pattern";
 
 fun dummy_pattern T = Const (dummy_patternN, T);
+val dummy = dummy_pattern dummyT;
+val dummy_prop = dummy_pattern propT;
 
 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
   | is_dummy_pattern _ = false;
@@ -979,7 +983,7 @@
 fun is_replaced_dummy_pattern ("_dummy_", _) = true
   | is_replaced_dummy_pattern _ = false;
 
-fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
+fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T
   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
   | show_dummy_patterns a = a;

--- a/src/Tools/induct.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/Tools/induct.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -642,9 +642,9 @@
 local
 
 fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
-  | goal_prefix 0 _ = Term.dummy_pattern propT
+  | goal_prefix 0 _ = Term.dummy_prop
   | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
-  | goal_prefix _ _ = Term.dummy_pattern propT;
+  | goal_prefix _ _ = Term.dummy_prop;
 
 fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
   | goal_params 0 _ = 0