src/HOL/Library/refute.ML
changeset 56846 9df717fef2bb
parent 56845 691da43fbdd4
child 56851 35ff4ede3409
     1.1 --- a/src/HOL/Library/refute.ML	Sun May 04 16:17:53 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Sun May 04 18:14:58 2014 +0200
     1.3 @@ -2399,7 +2399,7 @@
     1.4                              end
     1.5                          end
     1.6                        val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
     1.7 -                      (* sanity check: the size of 'IDT' should be 'idt_size' *)
     1.8 +                      (* sanity check: the size of 'IDT' should be 'size_idt' *)
     1.9                        val _ =
    1.10                            if idt_size <> size_of_type ctxt (typs, []) IDT then
    1.11                              raise REFUTE ("IDT_recursion_interpreter",