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