CONVERSION: handle TYPE | TERM | CTERM | THM;
authorwenzelm
Tue, 03 Jul 2007 22:27:30 +0200
changeset 23561 a531c8da8a9b
parent 23560 e43686246de4
child 23562 6cad6b400cfd
CONVERSION: handle TYPE | TERM | CTERM | THM;
src/Pure/tctical.ML
--- 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;