# HG changeset patch
# User chaieb
# Date 1183365799 -7200
# Node ID d52108dd4b6cec9e50209e1fc2600afbad9a9ad7
# Parent  7e8255828502a4199af11fa067282f505dd4e17d
Handle exception TYPE

diff -r 7e8255828502 -r d52108dd4b6c src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 02 10:43:17 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 02 10:43:19 2007 +0200
@@ -518,12 +518,13 @@
  fun conv ctxt p = 
   let val _ = () (* my_term := p *)
   in
-   Qelim.gen_qelim_conv ctxt pcv postcv pcv (cons o term_of) 
+   Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
       (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
       (cooperex_conv ctxt) p 
   end
   handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
         | THM s => raise COOPER ("Cooper Failed", THM s) 
+        | TYPE s => raise COOPER ("Cooper Failed", TYPE s) 
 in val cooper_conv = conv 
 end;
 end;