src/HOL/Tools/inductive_realizer.ML

      (case strip_type T of
         (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
       | _ => vs)) (Term.add_vars prop []) [];
 
 val attach_typeS = map_types (map_atyps
-  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
-    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
+  (fn TFree (s, []) => TFree (s, @{sort type})
+    | TVar (ixn, []) => TVar (ixn, @{sort type})
     | T => T));
 
 fun dt_of_intrs thy vs nparms intrs =
   let
     val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);