--- a/src/HOL/Library/Multiset.thy Fri Apr 10 12:16:45 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Apr 10 12:16:58 2015 +0200
@@ -2435,8 +2435,7 @@
unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
apply (rule ext)+
apply auto
- apply (rule_tac x = "multiset_of (zip xs ys)" in exI)
- apply auto[1]
+ apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto)
apply (metis list_all2_lengthD map_fst_zip multiset_of_map)
apply (auto simp: list_all2_iff)[1]
apply (metis list_all2_lengthD map_snd_zip multiset_of_map)
@@ -2448,7 +2447,8 @@
apply (rule_tac x = "map fst xys" in exI)
apply (auto simp: multiset_of_map)
apply (rule_tac x = "map snd xys" in exI)
- by (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
+ apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
+ done
next
show "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
by auto
--- a/src/HOL/Library/Sublist.thy Fri Apr 10 12:16:45 2015 +0200
+++ b/src/HOL/Library/Sublist.thy Fri Apr 10 12:16:58 2015 +0200
@@ -144,7 +144,7 @@
lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
apply (induct n arbitrary: xs ys)
- apply (case_tac ys, simp_all)[1]
+ apply (case_tac ys; simp)
apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
done
--- a/src/HOL/Num.thy Fri Apr 10 12:16:45 2015 +0200
+++ b/src/HOL/Num.thy Fri Apr 10 12:16:58 2015 +0200
@@ -1195,10 +1195,10 @@
declaration {*
let
- fun number_of thy T n =
- if not (Sign.of_sort thy (T, @{sort numeral}))
+ fun number_of ctxt T n =
+ if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
then raise CTERM ("number_of", [])
- else Numeral.mk_cnumber (Thm.global_ctyp_of thy T) n;
+ else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
in
K (
Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps}
--- a/src/HOL/Tools/int_arith.ML Fri Apr 10 12:16:45 2015 +0200
+++ b/src/HOL/Tools/int_arith.ML Fri Apr 10 12:16:58 2015 +0200
@@ -79,10 +79,10 @@
make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
proc = sproc, identifier = []}
-fun number_of thy T n =
- if not (Sign.of_sort thy (T, @{sort numeral}))
+fun number_of ctxt T n =
+ if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
then raise CTERM ("number_of", [])
- else Numeral.mk_cnumber (Thm.global_ctyp_of thy T) n;
+ else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
val setup =
Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
--- a/src/HOL/Tools/lin_arith.ML Fri Apr 10 12:16:45 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Apr 10 12:16:58 2015 +0200
@@ -16,7 +16,7 @@
val add_simprocs: simproc list -> Context.generic -> Context.generic
val add_inj_const: string * typ -> Context.generic -> Context.generic
val add_discrete_type: string -> Context.generic -> Context.generic
- val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
+ val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
val setup: Context.generic -> Context.generic
val global_setup: theory -> theory
val split_limit: int Config.T
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Apr 10 12:16:45 2015 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Apr 10 12:16:58 2015 +0200
@@ -91,16 +91,16 @@
val map_data:
({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
lessD: thm list, neqE: thm list, simpset: simpset,
- number_of: (theory -> typ -> int -> cterm) option} ->
+ number_of: (Proof.context -> typ -> int -> cterm) option} ->
{add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
lessD: thm list, neqE: thm list, simpset: simpset,
- number_of: (theory -> typ -> int -> cterm) option}) ->
+ number_of: (Proof.context -> typ -> int -> cterm) option}) ->
Context.generic -> Context.generic
val add_inj_thms: thm list -> Context.generic -> Context.generic
val add_lessD: thm -> Context.generic -> Context.generic
val add_simps: thm list -> Context.generic -> Context.generic
val add_simprocs: simproc list -> Context.generic -> Context.generic
- val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
+ val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
end;
functor Fast_Lin_Arith
@@ -119,7 +119,7 @@
lessD: thm list,
neqE: thm list,
simpset: simpset,
- number_of: (theory -> typ -> int -> cterm) option};
+ number_of: (Proof.context -> typ -> int -> cterm) option};
val empty : T =
{add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
@@ -169,7 +169,7 @@
fun number_of ctxt =
(case Data.get (Context.Proof ctxt) of
- {number_of = SOME f, ...} => f (Proof_Context.theory_of ctxt)
+ {number_of = SOME f, ...} => f ctxt
| _ => fn _ => fn _ => raise CTERM ("number_of", []));
--- a/src/Pure/drule.ML Fri Apr 10 12:16:45 2015 +0200
+++ b/src/Pure/drule.ML Fri Apr 10 12:16:58 2015 +0200
@@ -204,10 +204,12 @@
val ps = outer_params (Thm.term_of goal)
|> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
val Ts = map Term.fastype_of ps;
- val inst = Thm.fold_terms Term.add_vars th [] |> map (fn (xi, T) =>
- (Thm.global_cterm_of thy (Var (xi, T)), Thm.global_cterm_of thy (Term.list_comb (Var (xi, Ts ---> T), ps))));
+ val inst =
+ Thm.fold_terms Term.add_vars th []
+ |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
in
- th |> Thm.instantiate ([], inst)
+ th
+ |> Thm.instantiate (Thm.certify_inst thy ([], inst))
|> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy) ps
end;
@@ -228,12 +230,10 @@
| zero_var_indexes_list ths =
let
val thy = Theory.merge_list (map Thm.theory_of_thm ths);
- val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
- val cinstT =
- map (fn (v, T) => (Thm.global_ctyp_of thy (TVar v), Thm.global_ctyp_of thy T)) instT;
- val cinst =
- map (fn (v, t) => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy t)) inst;
- in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
+ val inst =
+ Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths)
+ |> Thm.certify_inst thy;
+ in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate inst) ths end;
val zero_var_indexes = singleton zero_var_indexes_list;
@@ -629,9 +629,9 @@
let
val thy = Thm.theory_of_cterm ct;
val T = Thm.typ_of_cterm ct;
- val a = Thm.global_ctyp_of thy (TVar (("'a", 0), []));
+ val instT = apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), []), T);
val x = Thm.global_cterm_of thy (Var (("x", 0), T));
- in Thm.instantiate ([(a, Thm.global_ctyp_of thy T)], [(x, ct)]) termI end;
+ in Thm.instantiate ([instT], [(x, ct)]) termI end;
fun dest_term th =
let val cprop = strip_imp_concl (Thm.cprop_of th) in