added Term.dummy_pattern conveniences;
authorwenzelm
Sun Oct 16 18:48:30 2011 +0200 (2011-10-16)
changeset 45156a9b6c2ea7bec
parent 45155 3216d65d8f34
child 45157 efc2e2d80218
added Term.dummy_pattern conveniences;
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Function/function_lib.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/drule.ML
src/Pure/proofterm.ML
src/Pure/term.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Sun Oct 16 16:56:01 2011 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sun Oct 16 18:48:30 2011 +0200
     1.3 @@ -346,7 +346,7 @@
     1.4                    (fold_rev count_cases cases []);
     1.5                  val R = type_of t;
     1.6                  val dummy =
     1.7 -                  if d then Const (@{const_name dummy_pattern}, R)
     1.8 +                  if d then Term.dummy_pattern R
     1.9                    else Free (singleton (Name.variant_list used) "x", R);
    1.10                in
    1.11                  SOME (x,
     2.1 --- a/src/HOL/Tools/Function/function_lib.ML	Sun Oct 16 16:56:01 2011 +0200
     2.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Sun Oct 16 18:48:30 2011 +0200
     2.3 @@ -75,9 +75,7 @@
     2.4    let
     2.5      val allthm = Thm.forall_intr cv thm
     2.6      val (_ $ abs) = prop_of allthm
     2.7 -  in
     2.8 -    Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
     2.9 -  end
    2.10 +  in Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy)) allthm end
    2.11  
    2.12  
    2.13  datatype proof_attempt = Solved of thm | Stuck of thm | Fail
     3.1 --- a/src/Pure/Proof/proof_syntax.ML	Sun Oct 16 16:56:01 2011 +0200
     3.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Oct 16 18:48:30 2011 +0200
     3.3 @@ -172,12 +172,12 @@
     3.4          Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
     3.5        end
     3.6    | term_of Ts (AbsP (s, t, prf)) =
     3.7 -      AbsPt $ the_default (Term.dummy_pattern propT) t $
     3.8 +      AbsPt $ the_default Term.dummy_prop t $
     3.9          Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
    3.10    | term_of Ts (prf1 %% prf2) =
    3.11        AppPt $ term_of Ts prf1 $ term_of Ts prf2
    3.12    | term_of Ts (prf % opt) =
    3.13 -      let val t = the_default (Term.dummy_pattern dummyT) opt
    3.14 +      let val t = the_default Term.dummy opt
    3.15        in Const ("Appt",
    3.16          [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
    3.17            term_of Ts prf $ t
     4.1 --- a/src/Pure/drule.ML	Sun Oct 16 16:56:01 2011 +0200
     4.2 +++ b/src/Pure/drule.ML	Sun Oct 16 18:48:30 2011 +0200
     4.3 @@ -729,7 +729,7 @@
     4.4  fun cterm_rule f = dest_term o f o mk_term;
     4.5  fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));
     4.6  
     4.7 -val dummy_thm = mk_term (certify (Term.dummy_pattern propT));
     4.8 +val dummy_thm = mk_term (certify Term.dummy_prop);
     4.9  
    4.10  
    4.11  (* sort_constraint *)
     5.1 --- a/src/Pure/proofterm.ML	Sun Oct 16 16:56:01 2011 +0200
     5.2 +++ b/src/Pure/proofterm.ML	Sun Oct 16 18:48:30 2011 +0200
     5.3 @@ -1051,10 +1051,8 @@
     5.4  
     5.5  val axm_proof = gen_axm_proof PAxm;
     5.6  
     5.7 -val dummy = Const (Term.dummy_patternN, dummyT);
     5.8 -
     5.9  fun oracle_proof name prop =
    5.10 -  if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
    5.11 +  if ! proofs = 0 then ((name, Term.dummy), Oracle (name, Term.dummy, NONE))
    5.12    else ((name, prop), gen_axm_proof Oracle name prop);
    5.13  
    5.14  fun shrink_proof thy =
     6.1 --- a/src/Pure/term.ML	Sun Oct 16 16:56:01 2011 +0200
     6.2 +++ b/src/Pure/term.ML	Sun Oct 16 18:48:30 2011 +0200
     6.3 @@ -164,6 +164,8 @@
     6.4    val dest_abs: string * typ * term -> string * term
     6.5    val dummy_patternN: string
     6.6    val dummy_pattern: typ -> term
     6.7 +  val dummy: term
     6.8 +  val dummy_prop: term
     6.9    val is_dummy_pattern: term -> bool
    6.10    val free_dummy_patterns: term -> Name.context -> term * Name.context
    6.11    val no_dummy_patterns: term -> term
    6.12 @@ -941,6 +943,8 @@
    6.13  val dummy_patternN = "dummy_pattern";
    6.14  
    6.15  fun dummy_pattern T = Const (dummy_patternN, T);
    6.16 +val dummy = dummy_pattern dummyT;
    6.17 +val dummy_prop = dummy_pattern propT;
    6.18  
    6.19  fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
    6.20    | is_dummy_pattern _ = false;
    6.21 @@ -979,7 +983,7 @@
    6.22  fun is_replaced_dummy_pattern ("_dummy_", _) = true
    6.23    | is_replaced_dummy_pattern _ = false;
    6.24  
    6.25 -fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
    6.26 +fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T
    6.27    | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
    6.28    | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
    6.29    | show_dummy_patterns a = a;
     7.1 --- a/src/Tools/induct.ML	Sun Oct 16 16:56:01 2011 +0200
     7.2 +++ b/src/Tools/induct.ML	Sun Oct 16 18:48:30 2011 +0200
     7.3 @@ -642,9 +642,9 @@
     7.4  local
     7.5  
     7.6  fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
     7.7 -  | goal_prefix 0 _ = Term.dummy_pattern propT
     7.8 +  | goal_prefix 0 _ = Term.dummy_prop
     7.9    | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
    7.10 -  | goal_prefix _ _ = Term.dummy_pattern propT;
    7.11 +  | goal_prefix _ _ = Term.dummy_prop;
    7.12  
    7.13  fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
    7.14    | goal_params 0 _ = 0