# HG changeset patch
# User wenzelm
# Date 1183494450 -7200
# Node ID a531c8da8a9b810fc7330b7c19c5910cb3592ee1
# Parent  e43686246de4cc915956b3d43105e0eb6343b77a
CONVERSION: handle TYPE | TERM | CTERM | THM;

diff -r e43686246de4 -r a531c8da8a9b 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;