src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 33810 38375b16ffd9
parent 33801 e8535acd302c
child 33971 9c7fa7f76950
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 22:25:11 2009 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 22:28:36 2009 -0800
     1.3 @@ -998,7 +998,7 @@
     1.4        handle THM _ =>
     1.5               (warning "Induction proofs failed (THM raised)."; ([], TrueI))
     1.6             | ERROR _ =>
     1.7 -             (warning "Induction proofs failed (ERROR raised)."; ([], TrueI));
     1.8 +             (warning "Cannot prove induction rule"; ([], TrueI));
     1.9  
    1.10  
    1.11  end; (* local *)