Handle exception TYPE
authorchaieb
Mon Jul 02 10:43:19 2007 +0200 (2007-07-02)
changeset 23523d52108dd4b6c
parent 23522 7e8255828502
child 23524 123a45589e0a
Handle exception TYPE
src/HOL/Tools/Qelim/cooper.ML
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 02 10:43:17 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 02 10:43:19 2007 +0200
     1.3 @@ -518,12 +518,13 @@
     1.4   fun conv ctxt p = 
     1.5    let val _ = () (* my_term := p *)
     1.6    in
     1.7 -   Qelim.gen_qelim_conv ctxt pcv postcv pcv (cons o term_of) 
     1.8 +   Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
     1.9        (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
    1.10        (cooperex_conv ctxt) p 
    1.11    end
    1.12    handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
    1.13          | THM s => raise COOPER ("Cooper Failed", THM s) 
    1.14 +        | TYPE s => raise COOPER ("Cooper Failed", TYPE s) 
    1.15  in val cooper_conv = conv 
    1.16  end;
    1.17  end;