--- a/src/Pure/term.ML Wed Sep 26 20:50:34 2007 +0200
+++ b/src/Pure/term.ML Wed Sep 26 22:20:59 2007 +0200
@@ -190,6 +190,7 @@
val dummy_patternN: string
val dummy_pattern: typ -> term
val is_dummy_pattern: term -> bool
+ val free_dummy_patterns: term -> Name.context -> term * Name.context
val no_dummy_patterns: term -> term
val replace_dummy_patterns: int * term -> int * term
val is_replaced_dummy_pattern: indexname -> bool
@@ -1250,6 +1251,19 @@
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 =
+ let val [x] = Name.invents used "uu" 1
+ in (Free (Name.internal x, T), Name.declare x used) end
+ | free_dummy_patterns (Abs (x, T, b)) used =
+ let val (b', used') = free_dummy_patterns b used
+ in (Abs (x, T, b'), used') end
+ | free_dummy_patterns (t $ u) used =
+ let
+ val (t', used') = free_dummy_patterns t used;
+ val (u', used'') = free_dummy_patterns u used';
+ in (t' $ u', used'') end
+ | free_dummy_patterns a used = (a, used);
+
fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
(i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
| replace_dummy Ts (i, Abs (x, T, t)) =