src/HOL/cladata.ML
changeset 4179 cc4b6791d5dc
parent 4085 6e2d41a5ea43
child 4205 96632970d203
     1.1 --- a/src/HOL/cladata.ML	Thu Nov 06 10:28:20 1997 +0100
     1.2 +++ b/src/HOL/cladata.ML	Thu Nov 06 10:29:37 1997 +0100
     1.3 @@ -14,7 +14,8 @@
     1.4    struct
     1.5    structure Simplifier = Simplifier
     1.6    (*Take apart an equality judgement; otherwise raise Match!*)
     1.7 -  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
     1.8 +  fun dest_eq (Const("Trueprop",_) $ (Const("op =",T)  $ t $ u)) = 
     1.9 +	(t, u, domain_type T)
    1.10    val eq_reflection = eq_reflection
    1.11    val imp_intr = impI
    1.12    val rev_mp = rev_mp