diff -r e64ff1c1bc70 -r cc4b6791d5dc src/HOL/cladata.ML --- 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