| changeset 4179 | cc4b6791d5dc |
| parent 4096 | 8cdf672a83e8 |
| child 4222 | d7573d6d0513 |
--- a/src/FOL/ROOT.ML Thu Nov 06 10:28:20 1997 +0100 +++ b/src/FOL/ROOT.ML Thu Nov 06 10:29:37 1997 +0100 @@ -27,7 +27,8 @@ struct structure Simplifier = Simplifier (*Take apart an equality judgement; otherwise raise Match!*) - fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u) + fun dest_eq (Const("Trueprop",_) $ (Const("op =",T) $ t $ u)) = + (t, u, domain_type T) val eq_reflection = eq_reflection val imp_intr = impI val rev_mp = rev_mp