src/HOL/Tools/Qelim/qelim.ML
changeset 36945 9bec62c10714
parent 35410 1ea89d2a1bd4
child 38786 e46e7a9cb622
     1.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4       val p = Thm.dest_arg p
     1.5       val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
     1.6       val th = instantiate' [SOME T] [SOME p] all_not_ex
     1.7 -    in transitive th (conv env (Thm.rhs_of th))
     1.8 +    in Thm.transitive th (conv env (Thm.rhs_of th))
     1.9      end
    1.10    | _ => atcv env p
    1.11   in precv then_conv (conv env) then_conv postcv end