src/HOL/Library/refute.ML

                             in
                               result
                             end
                         end
                       val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
-                      (* sanity check: the size of 'IDT' should be 'idt_size' *)
+                      (* sanity check: the size of 'IDT' should be 'size_idt' *)
                       val _ =
                           if idt_size <> size_of_type ctxt (typs, []) IDT then
                             raise REFUTE ("IDT_recursion_interpreter",
                               "unexpected size of IDT (wrong type associated?)")
                           else ()