tuned -- avoid slightly odd @{cpat};
authorwenzelm
Tue Sep 01 17:25:36 2015 +0200 (2015-09-01)
changeset 61075f6b0d827240e
parent 61074 44a8cd035dfb
child 61076 bdc1e2f0a86a
tuned -- avoid slightly odd @{cpat};
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/semiring_normalizer.ML
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Aug 31 22:45:40 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue Sep 01 17:25:36 2015 +0200
     1.3 @@ -902,15 +902,6 @@
     1.4    | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
     1.5    | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
     1.6  
     1.7 -fun mk_frac phi cT x =
     1.8 -  let val (a, b) = Rat.quotient_of_rat x
     1.9 -  in if b = 1 then Numeral.mk_cnumber cT a
    1.10 -    else Thm.apply
    1.11 -         (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
    1.12 -                     (Numeral.mk_cnumber cT a))
    1.13 -         (Numeral.mk_cnumber cT b)
    1.14 - end
    1.15 -
    1.16  fun whatis x ct = case Thm.term_of ct of
    1.17    Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ =>
    1.18       if y aconv Thm.term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
    1.19 @@ -973,9 +964,10 @@
    1.20     (case whatis x (Thm.dest_arg1 ct) of
    1.21      ("c*x+t",[c,t]) =>
    1.22         let
    1.23 -        val T = Thm.ctyp_of_cterm x
    1.24 +        val T = Thm.typ_of_cterm x
    1.25 +        val cT = Thm.ctyp_of_cterm x
    1.26          val cr = dest_frac c
    1.27 -        val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
    1.28 +        val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
    1.29          val cz = Thm.dest_arg ct
    1.30          val neg = cr </ Rat.zero
    1.31          val cthp = Simplifier.rewrite ctxt
    1.32 @@ -983,7 +975,7 @@
    1.33                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.34                      else Thm.apply (Thm.apply clt cz) c))
    1.35          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    1.36 -        val th = Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [c,x,t])
    1.37 +        val th = Thm.implies_elim (Thm.instantiate' [SOME cT] (map SOME [c,x,t])
    1.38               (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
    1.39          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.40                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.41 @@ -997,9 +989,10 @@
    1.42         in  rth end
    1.43      | ("c*x",[c]) =>
    1.44         let
    1.45 -        val T = Thm.ctyp_of_cterm x
    1.46 +        val T = Thm.typ_of_cterm x
    1.47 +        val cT = Thm.ctyp_of_cterm x
    1.48          val cr = dest_frac c
    1.49 -        val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
    1.50 +        val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
    1.51          val cz = Thm.dest_arg ct
    1.52          val neg = cr </ Rat.zero
    1.53          val cthp = Simplifier.rewrite ctxt
     2.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Mon Aug 31 22:45:40 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Tue Sep 01 17:25:36 2015 +0200
     2.3 @@ -206,7 +206,7 @@
     2.4     val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
     2.5     val postcv = Simplifier.rewrite (put_simpset ss ctxt);
     2.6     val nnf = K (nnf_conv ctxt then_conv postcv)
     2.7 -   val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Drule.cterm_add_frees tm [])
     2.8 +   val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm [])
     2.9                    (isolate_conv ctxt) nnf
    2.10                    (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
    2.11                                                 whatis = whatis, simpset = ss}) vs
     3.1 --- a/src/HOL/Decision_Procs/langford.ML	Mon Aug 31 22:45:40 2015 +0200
     3.2 +++ b/src/HOL/Decision_Procs/langford.ML	Tue Sep 01 17:25:36 2015 +0200
     3.3 @@ -190,7 +190,7 @@
     3.4            addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
     3.5    in
     3.6      fn p =>
     3.7 -      Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
     3.8 +      Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
     3.9          (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
    3.10          (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
    3.11    end;
    3.12 @@ -228,12 +228,12 @@
    3.13      (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm])
    3.14    | (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
    3.15  
    3.16 -fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    3.17 +fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    3.18    let
    3.19 -    fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
    3.20 -    fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
    3.21 -    val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
    3.22 -    val p' = fold_rev gen ts p
    3.23 +    fun all x t =
    3.24 +      Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
    3.25 +    val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
    3.26 +    val p' = fold_rev all ts p
    3.27    in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
    3.28  
    3.29  fun cfrees ats ct =
    3.30 @@ -259,7 +259,7 @@
    3.31        Object_Logic.full_atomize_tac ctxt i THEN
    3.32        simp_tac (put_simpset ss ctxt) i
    3.33        THEN (CONVERSION Thm.eta_long_conversion) i
    3.34 -      THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
    3.35 +      THEN (TRY o generalize_tac ctxt (cfrees (#atoms instance))) i
    3.36        THEN Object_Logic.full_atomize_tac ctxt i
    3.37        THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
    3.38        THEN (simp_tac (put_simpset ss ctxt) i)));
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Aug 31 22:45:40 2015 +0200
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue Sep 01 17:25:36 2015 +0200
     4.3 @@ -514,14 +514,15 @@
     4.4        | _ => "x"
     4.5  
     4.6      fun mk_forall x th =
     4.7 -      Drule.arg_cong_rule
     4.8 -        (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
     4.9 -        (Thm.abstract_rule (name_of x) x th)
    4.10 +      let
    4.11 +        val T = Thm.typ_of_cterm x
    4.12 +        val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool}))
    4.13 +      in Drule.arg_cong_rule all (Thm.abstract_rule (name_of x) x th) end
    4.14  
    4.15      val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
    4.16  
    4.17 -    fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
    4.18 -    fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
    4.19 +    fun ext T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool}))
    4.20 +    fun mk_ex v t = Thm.apply (ext (Thm.typ_of_cterm v)) (Thm.lambda v t)
    4.21  
    4.22      fun choose v th th' =
    4.23        case Thm.concl_of th of
     5.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Mon Aug 31 22:45:40 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Tue Sep 01 17:25:36 2015 +0200
     5.3 @@ -343,8 +343,14 @@
     5.4    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
     5.5    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
     5.6    fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
     5.7 -  fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
     5.8 -  fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
     5.9 +  fun mk_norm t =
    5.10 +    let val T = Thm.typ_of_cterm t
    5.11 +    in Thm.apply (Thm.cterm_of ctxt' (Const (@{const_name norm}, T --> @{typ real}))) t end
    5.12 +  fun mk_equals l r =
    5.13 +    let
    5.14 +      val T = Thm.typ_of_cterm l
    5.15 +      val eq = Thm.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT))
    5.16 +    in Thm.apply (Thm.apply eq l) r end
    5.17    val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Thm.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns
    5.18    val replace_conv = try_conv (rewrs_conv asl)
    5.19    val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
     6.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Aug 31 22:45:40 2015 +0200
     6.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Sep 01 17:25:36 2015 +0200
     6.3 @@ -569,7 +569,7 @@
     6.4        [not_all, all_not_ex, @{thm ex_disj_distrib}]));
     6.5  
     6.6  fun conv ctxt p =
     6.7 -  Qelim.gen_qelim_conv
     6.8 +  Qelim.gen_qelim_conv ctxt
     6.9      (Simplifier.rewrite (put_simpset conv_ss ctxt))
    6.10      (Simplifier.rewrite (put_simpset presburger_ss ctxt))
    6.11      (Simplifier.rewrite (put_simpset conv_ss ctxt))
    6.12 @@ -799,12 +799,12 @@
    6.13   in h [] ct end
    6.14  end;
    6.15  
    6.16 -fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    6.17 +fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    6.18   let 
    6.19 -   fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
    6.20 -   fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
    6.21 -   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
    6.22 -   val p' = fold_rev gen ts p
    6.23 +   fun all x t =
    6.24 +    Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
    6.25 +   val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
    6.26 +   val p' = fold_rev all ts p
    6.27   in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
    6.28  
    6.29  local
    6.30 @@ -875,7 +875,7 @@
    6.31      THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
    6.32      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    6.33      THEN_ALL_NEW simp_tac simpset_ctxt
    6.34 -    THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
    6.35 +    THEN_ALL_NEW (TRY o generalize_tac ctxt (int_nat_terms ctxt))
    6.36      THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
    6.37      THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
    6.38      THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
     7.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Mon Aug 31 22:45:40 2015 +0200
     7.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Tue Sep 01 17:25:36 2015 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  
     7.5  signature QELIM =
     7.6  sig
     7.7 - val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a ->
     7.8 + val gen_qelim_conv: Proof.context -> conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a ->
     7.9    ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
    7.10   val standard_qelim_conv: Proof.context ->
    7.11    (cterm list -> conv) -> (cterm list -> conv) ->
    7.12 @@ -18,7 +18,7 @@
    7.13  
    7.14  val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
    7.15  
    7.16 -fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =
    7.17 +fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv =
    7.18   let
    7.19    fun conv env p =
    7.20     case Thm.term_of p of
    7.21 @@ -41,10 +41,10 @@
    7.22      in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
    7.23         else Thm.transitive (Thm.transitive th th') (conv env r) end
    7.24    | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
    7.25 -  | Const(@{const_name All},_)$_ =>
    7.26 +  | Const(@{const_name All}, allT)$_ =>
    7.27      let
    7.28 +     val T = Thm.ctyp_of ctxt (#1 (Term.dest_funT (#1 (Term.dest_funT allT))))
    7.29       val p = Thm.dest_arg p
    7.30 -     val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
    7.31       val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
    7.32      in Thm.transitive th (conv env (Thm.rhs_of th))
    7.33      end
    7.34 @@ -65,7 +65,7 @@
    7.35  
    7.36  fun standard_qelim_conv ctxt atcv ncv qcv p =
    7.37    let val pcv = pcv ctxt
    7.38 -  in gen_qelim_conv pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
    7.39 +  in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
    7.40  
    7.41  end;
    7.42  
     8.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Mon Aug 31 22:45:40 2015 +0200
     8.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Sep 01 17:25:36 2015 +0200
     8.3 @@ -709,7 +709,8 @@
     8.4            (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
     8.5              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
     8.6          handle TERM (_, ts) => raise TERM (err_msg, ts)
     8.7 -    val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     8.8 +    val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), @{typ bool})))
     8.9 +    val thm3 = Goal.prove_internal ctxt' [] goal (K tac)
    8.10      val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
    8.11    in
    8.12      thm3
    8.13 @@ -746,7 +747,8 @@
    8.14            (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
    8.15              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
    8.16          handle TERM (_, ts) => raise TERM (err_msg, ts)
    8.17 -    val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
    8.18 +    val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), @{typ bool})))
    8.19 +    val thm3 = Goal.prove_internal ctxt' [] goal (K tac)
    8.20      val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
    8.21    in
    8.22      thm3
     9.1 --- a/src/HOL/Tools/groebner.ML	Mon Aug 31 22:45:40 2015 +0200
     9.2 +++ b/src/HOL/Tools/groebner.ML	Tue Sep 01 17:25:36 2015 +0200
     9.3 @@ -478,8 +478,8 @@
     9.4  
     9.5     (* Conversion for the equivalence of existential statements where
     9.6        EX quantifiers are rearranged differently *)
     9.7 - fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
     9.8 - fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
     9.9 +fun ext ctxt T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool}))
    9.10 +fun mk_ex ctxt v t = Thm.apply (ext ctxt (Thm.typ_of_cterm v)) (Thm.lambda v t)
    9.11  
    9.12  fun choose v th th' = case Thm.concl_of th of
    9.13    @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
    9.14 @@ -494,8 +494,8 @@
    9.15     in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
    9.16  | _ => error ""  (* FIXME ? *)
    9.17  
    9.18 -fun simple_choose v th =
    9.19 -   choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
    9.20 +fun simple_choose ctxt v th =
    9.21 +   choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex ctxt v)
    9.22      (Thm.dest_arg (hd (Thm.chyps_of th))))) th
    9.23  
    9.24  
    9.25 @@ -507,14 +507,14 @@
    9.26        (Thm.instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
    9.27        th
    9.28    end
    9.29 - fun ex_eq_conv t =
    9.30 + fun ex_eq_conv ctxt t =
    9.31    let
    9.32    val (p0,q0) = Thm.dest_binop t
    9.33    val (vs',P) = strip_exists p0
    9.34    val (vs,_) = strip_exists q0
    9.35     val th = Thm.assume (Thm.apply @{cterm Trueprop} P)
    9.36 -   val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th))
    9.37 -   val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
    9.38 +   val th1 = implies_intr_hyps (fold (simple_choose ctxt) vs' (fold mkexi vs th))
    9.39 +   val th2 = implies_intr_hyps (fold (simple_choose ctxt) vs (fold mkexi vs' th))
    9.40     val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1
    9.41     val q = (Thm.dest_arg o Thm.dest_arg o Thm.cprop_of) th1
    9.42    in Thm.implies_elim (Thm.implies_elim (Thm.instantiate' [] [SOME p, SOME q] iffI) th1) th2
    9.43 @@ -527,7 +527,7 @@
    9.44   | Var ((s,_),_) => s
    9.45   | _ => "x"
    9.46   fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
    9.47 -  fun mk_exists v th = Drule.arg_cong_rule (ext (Thm.ctyp_of_cterm v))
    9.48 + fun mk_exists ctxt v th = Drule.arg_cong_rule (ext ctxt (Thm.typ_of_cterm v))
    9.49     (Thm.abstract_rule (getname v) v th)
    9.50   fun simp_ex_conv ctxt =
    9.51     Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
    9.52 @@ -738,9 +738,10 @@
    9.53  fun ring ctxt tm =
    9.54   let
    9.55    fun mk_forall x p =
    9.56 -    Thm.apply
    9.57 -      (Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
    9.58 -        @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
    9.59 +    let
    9.60 +      val T = Thm.typ_of_cterm x;
    9.61 +      val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool}))
    9.62 +    in Thm.apply all (Thm.lambda x p) end
    9.63    val avs = Drule.cterm_add_frees tm []
    9.64    val P' = fold mk_forall avs tm
    9.65    val th1 = initial_conv ctxt (mk_neg P')
    9.66 @@ -829,9 +830,9 @@
    9.67        (Drule.binop_cong_rule @{cterm HOL.conj} th1
    9.68          (Thm.reflexive (Thm.dest_arg (Thm.rhs_of th2))))
    9.69    val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
    9.70 -  val th4 = Conv.fconv_rule (Conv.arg_conv (simp_ex_conv ctxt)) (mk_exists v th3)
    9.71 -  val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4)))
    9.72 - in Thm.transitive th5 (fold mk_exists (remove op aconvc v vars) th4)
    9.73 +  val th4 = Conv.fconv_rule (Conv.arg_conv (simp_ex_conv ctxt)) (mk_exists ctxt v th3)
    9.74 +  val th5 = ex_eq_conv ctxt (mk_eq tm (fold (mk_ex ctxt) (remove op aconvc v vars) (Thm.lhs_of th4)))
    9.75 + in Thm.transitive th5 (fold (mk_exists ctxt) (remove op aconvc v vars) th4)
    9.76   end;
    9.77  end
    9.78  
    10.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Mon Aug 31 22:45:40 2015 +0200
    10.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Tue Sep 01 17:25:36 2015 +0200
    10.3 @@ -123,6 +123,9 @@
    10.4        Simplifier.rewrite (put_simpset semiring_norm_ss ctxt)
    10.5        then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_1_eq_1}))};
    10.6  
    10.7 +val divide_const = Thm.cterm_of @{context} (Logic.varify_global @{term "op /"});
    10.8 +val [divide_tvar] = Term.add_tvars (Thm.term_of divide_const) [];
    10.9 +
   10.10  val field_funs =
   10.11    let
   10.12      fun numeral_is_const ct =
   10.13 @@ -142,7 +145,7 @@
   10.14        let val (a, b) = Rat.quotient_of_rat x
   10.15        in if b = 1 then Numeral.mk_cnumber cT a
   10.16          else Thm.apply
   10.17 -             (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
   10.18 +             (Thm.apply (Thm.instantiate_cterm ([(divide_tvar, cT)], []) divide_const)
   10.19                           (Numeral.mk_cnumber cT a))
   10.20               (Numeral.mk_cnumber cT b)
   10.21        end