--- 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)]);