changeset 187 | fcf8024c920d |
parent 152 | 7d8781fc2c8e |
--- a/intr_elim.ML Fri Nov 25 14:39:13 1994 +0100 +++ b/intr_elim.ML Fri Nov 25 16:24:18 1994 +0100 @@ -66,7 +66,7 @@ val mono = prove_goalw_cterm [] - (cterm_of sign (mk_tprop (Const("mono", monoT-->boolT) $ fp_abs))) + (cterm_of sign (mk_Trueprop (Const("mono", monoT-->boolT) $ fp_abs))) (fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)]);