--- a/src/HOL/Tools/inductive_realizer.ML Mon Jan 08 21:54:20 2024 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Jan 08 22:26:04 2024 +0100
@@ -52,10 +52,7 @@
(_, Type (s, _)) => if s = \<^type_name>\<open>bool\<close> then (a, T) :: vs else vs
| _ => vs)) (Term.add_vars prop []) [];
-val attach_typeS = map_types (map_atyps
- (fn TFree (s, []) => TFree (s, \<^sort>\<open>type\<close>)
- | TVar (ixn, []) => TVar (ixn, \<^sort>\<open>type\<close>)
- | T => T));
+val attach_typeS = Term.smash_sorts \<^sort>\<open>type\<close>;
fun dt_of_intrs thy vs nparms intrs =
let