# HG changeset patch
# User wenzelm
# Date 1570199145 -7200
# Node ID edaeb8feb4d069619769456d4ec6461b2ef7a861
# Parent  799437173553271829881469d52c59433873db23
proper replacement for (map_types (K dummyT));

diff -r 799437173553 -r edaeb8feb4d0 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Oct 04 15:30:52 2019 +0200
+++ b/src/Pure/consts.ML	Fri Oct 04 16:25:45 2019 +0200
@@ -30,6 +30,7 @@
   val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
+  val dummy_types: T -> term -> term
   val declare: Context.generic -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
   val abbreviate: Context.generic -> Type.tsig -> string -> binding * term -> T -> (term * term) * T
@@ -229,6 +230,17 @@
       raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
   in declT |> Term_Subst.instantiateT inst end;
 
+fun dummy_types consts =
+  let
+    fun dummy (Const (c, T)) =
+          Const (c, instance consts (c, replicate (length (typargs consts (c, T))) dummyT))
+      | dummy (Free (x, _)) = Free (x, dummyT)
+      | dummy (Var (xi, _)) = Var (xi, dummyT)
+      | dummy (b as Bound _) = b
+      | dummy (t $ u) = dummy t $ dummy u
+      | dummy (Abs (a, _, b)) = Abs (a, dummyT, dummy b);
+  in dummy end;
+
 
 
 (** build consts **)