src/Pure/logic.ML

--- a/src/Pure/logic.ML	Fri Nov 10 19:09:40 2000 +0100
+++ b/src/Pure/logic.ML	Fri Nov 10 19:10:34 2000 +0100
@@ -256,6 +256,7 @@
 fun has_meta_prems prop i =
   let
     fun is_meta (Const ("==>", _) $ _ $ _) = true
+      | is_meta (Const ("==", _) $ _ $ _) = true
       | is_meta (Const ("all", _) $ _) = true
       | is_meta _ = false;
     val horn = skip_flexpairs prop;