1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Apr 14 20:44:53 2012 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Apr 14 23:34:18 2012 +0200
     1.3 @@ -721,8 +721,12 @@
     1.4       val ntac = (case qs of [] => q aconvc @{cterm "False"}
     1.5                           | _ => false)
     1.6      in 
     1.7 -    if ntac then no_tac
     1.8 -      else rtac (Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) i
     1.9 +      if ntac then no_tac
    1.10 +      else
    1.11 +        (case try (fn () =>
    1.12 +            Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
    1.13 +          NONE => no_tac
    1.14 +        | SOME r => rtac r i)
    1.15      end)
    1.16  end;
    1.17  
    1.18 @@ -835,26 +839,27 @@
    1.19  fun finish_tac q = SUBGOAL (fn (_, i) =>
    1.20    (if q then I else TRY) (rtac TrueI i));
    1.21  
    1.22 -fun tac elim add_ths del_ths ctxt =
    1.23 -let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
    1.24 +fun tac elim add_ths del_ths = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} =>
    1.25 +  let
    1.26 +    val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
    1.27      val aprems = Arith_Data.get_arith_facts ctxt
    1.28 -in
    1.29 -  Method.insert_tac aprems
    1.30 -  THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.31 -  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.32 -  THEN_ALL_NEW simp_tac ss
    1.33 -  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
    1.34 -  THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.35 -  THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
    1.36 -  THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.37 -  THEN_ALL_NEW div_mod_tac ctxt
    1.38 -  THEN_ALL_NEW splits_tac ctxt
    1.39 -  THEN_ALL_NEW simp_tac ss
    1.40 -  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.41 -  THEN_ALL_NEW nat_to_int_tac ctxt
    1.42 -  THEN_ALL_NEW (core_tac ctxt)
    1.43 -  THEN_ALL_NEW finish_tac elim
    1.44 -end;
    1.45 +  in
    1.46 +    Method.insert_tac aprems
    1.47 +    THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.48 +    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.49 +    THEN_ALL_NEW simp_tac ss
    1.50 +    THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
    1.51 +    THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.52 +    THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
    1.53 +    THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.54 +    THEN_ALL_NEW div_mod_tac ctxt
    1.55 +    THEN_ALL_NEW splits_tac ctxt
    1.56 +    THEN_ALL_NEW simp_tac ss
    1.57 +    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.58 +    THEN_ALL_NEW nat_to_int_tac ctxt
    1.59 +    THEN_ALL_NEW (core_tac ctxt)
    1.60 +    THEN_ALL_NEW finish_tac elim
    1.61 +  end 1);
    1.62  
    1.63  
    1.64  (* theory setup *)