author | wenzelm |
Tue, 03 Jul 2007 22:27:30 +0200 | |
changeset 23561 | a531c8da8a9b |
parent 23560 | e43686246de4 |
child 23562 | 6cad6b400cfd |
--- a/src/Pure/tctical.ML Tue Jul 03 22:27:27 2007 +0200 +++ b/src/Pure/tctical.ML Tue Jul 03 22:27:30 2007 +0200 @@ -523,7 +523,10 @@ (*Conversions as tactics*) fun CONVERSION cv i st = Seq.single (Conv.goal_conv_rule cv i st) - handle THM _ => Seq.empty | CTERM _ => Seq.empty; + handle THM _ => Seq.empty + | CTERM _ => Seq.empty + | TERM _ => Seq.empty + | TYPE _ => Seq.empty; end;