| changeset 4179 | cc4b6791d5dc |
| parent 4085 | 6e2d41a5ea43 |
| child 4205 | 96632970d203 |
--- a/src/HOL/cladata.ML Thu Nov 06 10:28:20 1997 +0100 +++ b/src/HOL/cladata.ML Thu Nov 06 10:29:37 1997 +0100 @@ -14,7 +14,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