src/HOL/Tools/BNF/bnf_comp.ML

     (* TODO: check olive = length inners > 0,
                    forall inner from inners. ilive = live,
                    forall inner from inners. idead = dead  *)
 
     val (oDs, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
+      (Variable.invent_types (replicate odead @{sort type}) lthy);
     val (Dss, lthy2) = apfst (map (map TFree))
-      (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
+      (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
     val (Ass, lthy3) = apfst (replicate ilive o map TFree)
-      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
+      (Variable.invent_types (replicate ilive @{sort type}) lthy2);
     val As = if ilive > 0 then hd Ass else [];
     val Ass_repl = replicate olive As;
     val (Bs, names_lthy) = apfst (map TFree)
-      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
+      (Variable.invent_types (replicate ilive @{sort type}) lthy3);
     val Bss_repl = replicate olive Bs;
 
     val ((((fs', Qs'), Asets), xs), _) = names_lthy
       |> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs)
       ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)

     val nwits = nwits_of_bnf bnf;
 
     (* TODO: check 0 < n <= live *)
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+      (Variable.invent_types (replicate dead @{sort type}) lthy);
     val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+      (Variable.invent_types (replicate live @{sort type}) lthy1);
     val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
-      (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
+      (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
 
     val ((Asets, lives), _(*names_lthy*)) = lthy
       |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
       ||>> mk_Frees "x" (drop n As);
     val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;

     val nwits = nwits_of_bnf bnf;
 
     (* TODO: check 0 < n *)
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+      (Variable.invent_types (replicate dead @{sort type}) lthy);
     val ((newAs, As), lthy2) = apfst (chop n o map TFree)
-      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
+      (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
     val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
-      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
+      (Variable.invent_types (replicate (n + live) @{sort type}) lthy2);
 
     val (Asets, _(*names_lthy*)) = lthy
       |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
 
     val T = mk_T_of_bnf Ds As bnf;

 
     fun permute xs = permute_like_unique (op =) src dest xs;
     fun unpermute xs = permute_like_unique (op =) dest src xs;
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+      (Variable.invent_types (replicate dead @{sort type}) lthy);
     val (As, lthy2) = apfst (map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+      (Variable.invent_types (replicate live @{sort type}) lthy1);
     val (Bs, _(*lthy3*)) = apfst (map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
+      (Variable.invent_types (replicate live @{sort type}) lthy2);
 
     val (Asets, _(*names_lthy*)) = lthy
       |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
 
     val T = mk_T_of_bnf Ds As bnf;

   let
     val live = live_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
 
     val (As, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
+      (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
     val (Bs, _) = apfst (map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+      (Variable.invent_types (replicate live @{sort type}) lthy1);
 
     val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
       |> mk_Frees' "f" (map2 (curry op -->) As Bs)
       ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);