added free_dummy_patterns;
authorwenzelm
Wed Sep 26 22:20:59 2007 +0200 (2007-09-26)
changeset 2473359e0b49688fb
parent 24732 08c2dd5378c7
child 24734 ff617b6711f4
added free_dummy_patterns;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed Sep 26 20:50:34 2007 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Sep 26 22:20:59 2007 +0200
     1.3 @@ -190,6 +190,7 @@
     1.4    val dummy_patternN: string
     1.5    val dummy_pattern: typ -> term
     1.6    val is_dummy_pattern: term -> bool
     1.7 +  val free_dummy_patterns: term -> Name.context -> term * Name.context
     1.8    val no_dummy_patterns: term -> term
     1.9    val replace_dummy_patterns: int * term -> int * term
    1.10    val is_replaced_dummy_pattern: indexname -> bool
    1.11 @@ -1250,6 +1251,19 @@
    1.12    if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
    1.13    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
    1.14  
    1.15 +fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
    1.16 +      let val [x] = Name.invents used "uu" 1
    1.17 +      in (Free (Name.internal x, T), Name.declare x used) end
    1.18 +  | free_dummy_patterns (Abs (x, T, b)) used =
    1.19 +      let val (b', used') = free_dummy_patterns b used
    1.20 +      in (Abs (x, T, b'), used') end
    1.21 +  | free_dummy_patterns (t $ u) used =
    1.22 +      let
    1.23 +        val (t', used') = free_dummy_patterns t used;
    1.24 +        val (u', used'') = free_dummy_patterns u used';
    1.25 +      in (t' $ u', used'') end
    1.26 +  | free_dummy_patterns a used = (a, used);
    1.27 +
    1.28  fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
    1.29        (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
    1.30    | replace_dummy Ts (i, Abs (x, T, t)) =