src/HOL/Tools/Meson/meson_clausify.ML
changeset 42944 9e620869a576
parent 42747 f132d13fcf75
child 43324 2b47822868e4
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Sun May 22 14:51:41 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sun May 22 14:51:42 2011 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5  (* Converts an elim-rule into an equivalent theorem that does not have the
     1.6     predicate variable. Leaves other theorems unchanged. We simply instantiate
     1.7 -   the conclusion variable to False. (Cf. "transform_elim_term" in
     1.8 +   the conclusion variable to False. (Cf. "transform_elim_prop" in
     1.9     "Sledgehammer_Util".) *)
    1.10  fun transform_elim_theorem th =
    1.11    case concl_of th of    (*conclusion variable*)