has_meta_prems: include "==";
authorwenzelm
Fri Nov 10 19:10:34 2000 +0100 (2000-11-10)
changeset 104428ef083987af9
parent 10441 d727c39c4a4b
child 10443 0a68dc9edba5
has_meta_prems: include "==";
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Fri Nov 10 19:09:40 2000 +0100
     1.2 +++ b/src/Pure/logic.ML	Fri Nov 10 19:10:34 2000 +0100
     1.3 @@ -256,6 +256,7 @@
     1.4  fun has_meta_prems prop i =
     1.5    let
     1.6      fun is_meta (Const ("==>", _) $ _ $ _) = true
     1.7 +      | is_meta (Const ("==", _) $ _ $ _) = true
     1.8        | is_meta (Const ("all", _) $ _) = true
     1.9        | is_meta _ = false;
    1.10      val horn = skip_flexpairs prop;