src/HOL/Tools/Qelim/cooper.ML
changeset 35410 1ea89d2a1bd4
parent 35267 8dfd816713c6
child 36527 68a837d1a754
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sun Feb 28 22:30:51 2010 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Feb 28 23:51:31 2010 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  exception COOPER of string * exn;
     1.6  fun simp_thms_conv ctxt =
     1.7 -  Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps simp_thms);
     1.8 +  Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
     1.9  val FWD = Drule.implies_elim_list;
    1.10  
    1.11  val true_tm = @{cterm "True"};
    1.12 @@ -514,8 +514,8 @@
    1.13  
    1.14  local
    1.15   val pcv = Simplifier.rewrite
    1.16 -     (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4))
    1.17 -                      @ [not_all,all_not_ex, ex_disj_distrib]))
    1.18 +     (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
    1.19 +                      @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
    1.20   val postcv = Simplifier.rewrite presburger_ss
    1.21   fun conv ctxt p =
    1.22    let val _ = ()