src/HOL/Library/positivstellensatz.ML
changeset 37117 59cee8807c29
parent 36945 9bec62c10714
child 37598 893dcabf0c04
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue May 25 20:22:55 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue May 25 20:28:16 2010 +0200
     1.3 @@ -386,7 +386,7 @@
     1.4   fun real_ineq_conv th ct =
     1.5    let
     1.6     val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th 
     1.7 -      handle MATCH => raise CTERM ("real_ineq_conv", [ct]))
     1.8 +      handle Pattern.MATCH => raise CTERM ("real_ineq_conv", [ct]))
     1.9    in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th'))
    1.10    end 
    1.11    val [real_lt_conv, real_le_conv, real_eq_conv,