tuned op's
authornipkow
Wed Dec 20 19:17:37 2017 +0100 (17 months ago)
changeset 67230b2800da9eb8a
parent 67229 4ecf0ef70efb
child 67231 754952c12293
tuned op's
src/HOL/Tools/groebner.ML
     1.1 --- a/src/HOL/Tools/groebner.ML	Wed Dec 20 14:53:34 2017 +0100
     1.2 +++ b/src/HOL/Tools/groebner.ML	Wed Dec 20 19:17:37 2017 +0100
     1.3 @@ -899,7 +899,7 @@
     1.4    | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
     1.5    | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
     1.6    | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
     1.7 -  | \<^term>\<open>op \<Longrightarrow>\<close> $_$_ => find_args bounds tm
     1.8 +  | \<^term>\<open>Pure.imp\<close> $_$_ => find_args bounds tm
     1.9    | Const("op ==",_)$_$_ => find_args bounds tm  (* FIXME proper const name *)
    1.10    | \<^term>\<open>Trueprop\<close>$_ => find_term bounds (Thm.dest_arg tm)
    1.11    | _ => raise TERM ("find_term", []))