diff -r e275d520f49d -r 4a655e62ad34 src/HOL/Tools/ctr_sugar_util.ML --- a/src/HOL/Tools/ctr_sugar_util.ML Thu Nov 14 19:54:10 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar_util.ML Thu Nov 14 20:55:09 2013 +0100 @@ -36,6 +36,9 @@ (string * sort) list * Proof.context val variant_tfrees: string list -> Proof.context -> typ list * Proof.context + val typ_subst_nonatomic: (typ * typ) list -> typ -> typ + val subst_nonatomic_types: (typ * typ) list -> term -> term + val mk_predT: typ list -> typ val mk_pred1T: typ -> typ @@ -143,6 +146,17 @@ apfst (map TFree) o variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS); +(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*) +fun typ_subst_nonatomic [] = I + | typ_subst_nonatomic inst = + let + fun subst (Type (s, Ts)) = perhaps (AList.lookup (op =) inst) (Type (s, map subst Ts)) + | subst T = perhaps (AList.lookup (op =) inst) T; + in subst end; + +fun subst_nonatomic_types [] = I + | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst); + fun mk_predT Ts = Ts ---> HOLogic.boolT; fun mk_pred1T T = mk_predT [T];