| changeset 38864 | 4abe644fcea5 |
| parent 38549 | d0385f2764d8 |
| child 42284 | 326f57825e1a |
--- a/src/HOL/Library/reflection.ML Sat Aug 28 20:24:40 2010 +0800 +++ b/src/HOL/Library/reflection.ML Sat Aug 28 16:14:32 2010 +0200 @@ -82,7 +82,7 @@ fun rearrange congs = let fun P (_, th) = - let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th + let val @{term "Trueprop"}$(Const (@{const_name HOL.eq},_) $l$_) = concl_of th in can dest_Var l end val (yes,no) = List.partition P congs in no @ yes end