src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 38786 e46e7a9cb622
parent 38558 32ad17fe2b9c
child 38795 848be46708dc
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4     | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
     1.5     | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
     1.6     | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
     1.7 -   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
     1.8 +   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
     1.9     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    1.10     | Const ("==", _) $ _ $ _ => find_args bounds tm
    1.11     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)