# HG changeset patch
# User nipkow
# Date 1428661018 -7200
# Node ID 3fa68bacfa2ba7b159a55806a11754fc1b766fca
# Parent  90fb391a15c12e64e170b58bcab91c77e6c99368# Parent  c54d36be22ef7701f1dd674570eca8a623f07bc6
merged

diff -r c54d36be22ef -r 3fa68bacfa2b src/HOL/Library/Multiset.thy
--- 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
diff -r c54d36be22ef -r 3fa68bacfa2b src/HOL/Library/Sublist.thy
--- 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
 
diff -r c54d36be22ef -r 3fa68bacfa2b src/HOL/Num.thy
--- 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}
diff -r c54d36be22ef -r 3fa68bacfa2b src/HOL/Tools/int_arith.ML
--- 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]
diff -r c54d36be22ef -r 3fa68bacfa2b src/HOL/Tools/lin_arith.ML
--- 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
diff -r c54d36be22ef -r 3fa68bacfa2b src/Provers/Arith/fast_lin_arith.ML
--- 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", []));
 
 
diff -r c54d36be22ef -r 3fa68bacfa2b src/Pure/drule.ML
--- 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