Handle exception TYPE
authorchaieb
Mon, 02 Jul 2007 10:43:19 +0200
changeset 23523 d52108dd4b6c
parent 23522 7e8255828502
child 23524 123a45589e0a
Handle exception TYPE
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;