src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
changeset 56254 a2dd9200854d
parent 55535 10194808430d
child 57090 0224caba67ca
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -148,7 +148,7 @@
     1.4  
     1.5  val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
     1.6  
     1.7 -fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
     1.8 +fun mk_TFrees n = mk_TFrees' (replicate n @{sort type});
     1.9  
    1.10  fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
    1.11  fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
    1.12 @@ -169,7 +169,7 @@
    1.13  
    1.14  fun variant_tfrees ss =
    1.15    apfst (map TFree) o
    1.16 -    variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
    1.17 +    variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
    1.18  
    1.19  (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
    1.20  fun typ_subst_nonatomic [] = I