src/Pure/logic.ML
changeset 10442 8ef083987af9
parent 9684 6b7d7635a062
child 10816 8b2eafed6183
     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;