# HG changeset patch
# User wenzelm
# Date 973879834 -3600
# Node ID 8ef083987af93ec942babcc0cf98d97a477875dc
# Parent  d727c39c4a4b102df143e1a1ff28074c855eccda
has_meta_prems: include "==";

diff -r d727c39c4a4b -r 8ef083987af9 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;