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,

     2.1 --- a/src/HOL/Library/reflection.ML	Tue May 25 20:22:55 2010 +0200
     2.2 +++ b/src/HOL/Library/reflection.ML	Tue May 25 20:28:16 2010 +0200
     2.3 @@ -140,24 +140,25 @@
     2.4                     bds)
     2.5                 end)
     2.6             | _ => da (s,ctxt) bds)
     2.7 -      in (case cgns of
     2.8 +      in
     2.9 +        (case cgns of
    2.10            [] => tryabsdecomp (t,ctxt) bds
    2.11 -        | ((vns,cong)::congs) => ((let
    2.12 -            val cert = cterm_of thy
    2.13 -            val certy = ctyp_of thy
    2.14 -            val (tyenv, tmenv) =
    2.15 -              Pattern.match thy
    2.16 -                ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
    2.17 -                (Vartab.empty, Vartab.empty)
    2.18 -            val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv)
    2.19 -            val (fts,its) =
    2.20 -              (map (snd o snd) fnvs,
    2.21 -               map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    2.22 -            val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
    2.23 -          in ((fts ~~ (replicate (length fts) ctxt),
    2.24 -               Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
    2.25 -          end)
    2.26 -        handle MATCH => decomp_genreif da congs (t,ctxt) bds))
    2.27 +        | ((vns,cong)::congs) =>
    2.28 +            (let
    2.29 +              val cert = cterm_of thy
    2.30 +              val certy = ctyp_of thy
    2.31 +              val (tyenv, tmenv) =
    2.32 +                Pattern.match thy
    2.33 +                  ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
    2.34 +                  (Vartab.empty, Vartab.empty)
    2.35 +              val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv)
    2.36 +              val (fts,its) =
    2.37 +                (map (snd o snd) fnvs,
    2.38 +                 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    2.39 +              val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
    2.40 +            in ((fts ~~ (replicate (length fts) ctxt),
    2.41 +                 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
    2.42 +            end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
    2.43        end;
    2.44  
    2.45   (* looks for the atoms equation and instantiates it with the right number *)
    2.46 @@ -231,7 +232,7 @@
    2.47                in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts)  end
    2.48              val th = (instantiate (subst_ty, substt)  eq) RS sym
    2.49            in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
    2.50 -          handle MATCH => tryeqs eqs bds)
    2.51 +          handle Pattern.MATCH => tryeqs eqs bds)
    2.52        in tryeqs (filter isat eqs) bds end), bds);
    2.53  
    2.54    (* Generic reification procedure: *)

     3.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue May 25 20:22:55 2010 +0200
     3.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue May 25 20:28:16 2010 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4    val get: Proof.context -> entry
     3.5    val del: term list -> attribute
     3.6    val add: term list -> attribute 
     3.7 +  exception COOPER of string
     3.8    val conv: Proof.context -> conv
     3.9    val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
    3.10    val method: (Proof.context -> Method.method) context_parser

     4.1 --- a/src/HOL/Tools/refute.ML	Tue May 25 20:22:55 2010 +0200
     4.2 +++ b/src/HOL/Tools/refute.ML	Tue May 25 20:28:16 2010 +0200
     4.3 @@ -588,7 +588,7 @@
     4.4          | NONE =>
     4.5            get_typedef_ax axioms
     4.6        end handle ERROR _         => get_typedef_ax axioms
     4.7 -               | MATCH           => get_typedef_ax axioms
     4.8 +               | TERM _          => get_typedef_ax axioms
     4.9                 | Type.TYPE_MATCH => get_typedef_ax axioms)
    4.10    in
    4.11      get_typedef_ax (Theory.all_axioms_of thy)

     5.1 --- a/src/HOL/Word/WordArith.thy	Tue May 25 20:22:55 2010 +0200
     5.2 +++ b/src/HOL/Word/WordArith.thy	Tue May 25 20:28:16 2010 +0200
     5.3 @@ -512,7 +512,9 @@
     5.4  
     5.5  fun uint_arith_tacs ctxt = 
     5.6    let
     5.7 -    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
     5.8 +    fun arith_tac' n t =
     5.9 +      Arith_Data.verbose_arith_tac ctxt n t
    5.10 +        handle Cooper.COOPER _ => Seq.empty;
    5.11      val cs = claset_of ctxt;
    5.12      val ss = simpset_of ctxt;
    5.13    in 
    5.14 @@ -1074,7 +1076,9 @@
    5.15  
    5.16  fun unat_arith_tacs ctxt =   
    5.17    let
    5.18 -    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
    5.19 +    fun arith_tac' n t =
    5.20 +      Arith_Data.verbose_arith_tac ctxt n t
    5.21 +        handle Cooper.COOPER _ => Seq.empty;
    5.22      val cs = claset_of ctxt;
    5.23      val ss = simpset_of ctxt;
    5.24    in