# HG changeset patch
# User wenzelm
# Date 1389548526 -3600
# Node ID 81fff1c659438520fd02bbce86bc34fb87801ac8
# Parent  0fd6b06602420731a4d31d2fbe3d80d301ce1f8f# Parent  f26a7f06266d820498f906175ca42bdab818a378
merged

diff -r 0fd6b0660242 -r 81fff1c65943 NEWS
--- a/NEWS	Sat Jan 11 21:03:11 2014 +0100
+++ b/NEWS	Sun Jan 12 18:42:06 2014 +0100
@@ -31,6 +31,14 @@
 "isabelle jedit -m MODE".
 
 
+*** Pure ***
+
+* More thorough check of proof context for goal statements and
+attributed fact expressions: background theory, declared hyps,
+declared variable names.  Potential INCOMPATIBILITY, tools need to
+observe standard context discipline.
+
+
 *** HOL ***
 
 * "declare [[code abort: ...]]" replaces "code_abort ...".
diff -r 0fd6b0660242 -r 81fff1c65943 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/FOL/simpdata.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -123,7 +123,7 @@
   |> Simplifier.set_mkcong mk_meta_cong
   |> simpset_of;
 
-fun unfold_tac ths ctxt =
+fun unfold_tac ctxt ths =
   ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths));
 
 
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -186,10 +186,10 @@
 fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
   if null set_maps then atac 1
   else
-    unfold_tac [in_rel] ctxt THEN
+    unfold_tac ctxt [in_rel] THEN
     REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
     hyp_subst_tac ctxt 1 THEN
-    unfold_tac set_maps ctxt THEN
+    unfold_tac ctxt set_maps THEN
     EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
       CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
 
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -782,7 +782,7 @@
 fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
   let val n = length ks;
   in
-    unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN
+    unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
     EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
       EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
         EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -580,7 +580,7 @@
       (map (map (rulify_term thy #> rpair [])) vc_compat)
   end;
 
-fun prove_eqvt s xatoms ctxt =
+fun prove_eqvt s xatoms ctxt =  (* FIXME ctxt should be called lthy *)
   let
     val thy = Proof_Context.theory_of ctxt;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
@@ -609,21 +609,21 @@
          atoms)
       end;
     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
-    val eqvt_simpset = put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps
-      (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
-      [mk_perm_bool_simproc names,
-       NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val (([t], [pi]), ctxt') = ctxt |>
       Variable.import_terms false [concl_of raw_induct] ||>>
       Variable.variant_fixes ["pi"];
+    val eqvt_simpset = put_simpset HOL_basic_ss ctxt' addsimps
+      (NominalThmDecls.get_eqvt_thms ctxt' @ perm_pi_simp) addsimprocs
+      [mk_perm_bool_simproc names,
+       NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val ps = map (fst o HOLogic.dest_imp)
       (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
-    fun eqvt_tac ctxt'' pi (intr, vs) st =
+    fun eqvt_tac pi (intr, vs) st =
       let
         fun eqvt_err s =
-          let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt
+          let val ([t], ctxt'') = Variable.import_terms true [prop_of intr] ctxt'
           in error ("Could not prove equivariance for introduction rule\n" ^
-            Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
+            Syntax.string_of_term ctxt'' t ^ "\n" ^ s)
           end;
         val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
           let
@@ -639,7 +639,7 @@
       in
         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
           NONE => eqvt_err ("Rule does not match goal\n" ^
-            Syntax.string_of_term ctxt'' (hd (prems_of st)))
+            Syntax.string_of_term ctxt' (hd (prems_of st)))
         | SOME (th, _) => Seq.single th
       end;
     val thss = map (fn atom =>
@@ -654,9 +654,9 @@
               HOLogic.mk_imp (p, list_comb (h, ts1 @
                 map (NominalDatatype.mk_perm [] pi') ts2))
             end) ps)))
-          (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
+          (fn _ => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
               full_simp_tac eqvt_simpset 1 THEN
-              eqvt_tac context pi' intr_vs) intrs')) |>
+              eqvt_tac pi' intr_vs) intrs')) |>
           singleton (Proof_Context.export ctxt' ctxt)))
       end) atoms
   in
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -12,6 +12,7 @@
 
 signature NOMINAL_THMDECLS =
 sig
+  val nominal_eqvt_debug: bool Config.T
   val eqvt_add: attribute
   val eqvt_del: attribute
   val eqvt_force_add: attribute
@@ -69,7 +70,6 @@
 
 fun get_derived_thm ctxt hyp concl orig_thm pi typi =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val pi' = Var (pi, typi);
     val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
     val ([goal_term, pi''], ctxt') = Variable.import_terms false
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Set.thy	Sun Jan 12 18:42:06 2014 +0100
@@ -69,9 +69,9 @@
 *}
 
 simproc_setup defined_Collect ("{x. P x & Q x}") = {*
-  fn _ =>
-    Quantifier1.rearrange_Collect
-     (rtac @{thm Collect_cong} 1 THEN
+  fn _ => Quantifier1.rearrange_Collect
+    (fn _ =>
+      rtac @{thm Collect_cong} 1 THEN
       rtac @{thm iffI} 1 THEN
       ALLGOALS
         (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
@@ -355,17 +355,17 @@
 *}
 
 simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*
-  let
-    val unfold_bex_tac = unfold_tac @{thms Bex_def};
-    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
-  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
+  fn _ => Quantifier1.rearrange_bex
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Bex_def} THEN
+      Quantifier1.prove_one_point_ex_tac)
 *}
 
 simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
-  let
-    val unfold_ball_tac = unfold_tac @{thms Ball_def};
-    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
-  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
+  fn _ => Quantifier1.rearrange_ball
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Ball_def} THEN
+      Quantifier1.prove_one_point_all_tac)
 *}
 
 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -122,19 +122,14 @@
 
 (* General reduction pair application *)
 fun rem_inv_img ctxt =
-  let
-    val unfold_tac = Local_Defs.unfold_tac ctxt
-  in
-    rtac @{thm subsetI} 1
-    THEN etac @{thm CollectE} 1
-    THEN REPEAT (etac @{thm exE} 1)
-    THEN unfold_tac @{thms inv_image_def}
-    THEN rtac @{thm CollectI} 1
-    THEN etac @{thm conjE} 1
-    THEN etac @{thm ssubst} 1
-    THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
-                     @ @{thms sum.cases})
-  end
+  rtac @{thm subsetI} 1
+  THEN etac @{thm CollectE} 1
+  THEN REPEAT (etac @{thm exE} 1)
+  THEN Local_Defs.unfold_tac ctxt @{thms inv_image_def}
+  THEN rtac @{thm CollectI} 1
+  THEN etac @{thm conjE} 1
+  THEN etac @{thm ssubst} 1
+  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.cases}
 
 (* Sets *)
 
@@ -289,9 +284,8 @@
          THEN (rtac @{thm rp_inv_image_rp} 1)
          THEN (rtac (order_rpair ms_rp label) 1)
          THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
-         THEN unfold_tac @{thms rp_inv_image_def} ctxt
-         THEN Local_Defs.unfold_tac ctxt
-           (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
+         THEN unfold_tac ctxt @{thms rp_inv_image_def}
+         THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
          THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
          THEN EVERY (map (prove_lev true) sl)
          THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -103,7 +103,8 @@
         Drule.cterm_instantiate subst relcomppI
       end
 
-    fun zip_transfer_rules ctxt thm =       let
+    fun zip_transfer_rules ctxt thm =
+      let
         val thy = Proof_Context.theory_of ctxt
         fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
         val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm
@@ -122,7 +123,8 @@
     val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
     val assms = cprems_of fixed_thm
     val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
-    val ctxt = Context.proof_map(fold (add_transfer_rule o Thm.assume) assms) ctxt
+    val (prems, ctxt) = fold_map Thm.assume_hyps assms ctxt
+    val ctxt = Context.proof_map (fold add_transfer_rule prems) ctxt
     val zipped_thm =
       fixed_thm
       |> undisch_all
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -70,9 +70,8 @@
 (*Is this the best way to invoke the simplifier??*)
 fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
 
-fun join_assums th =
+fun join_assums ctxt th =
   let val thy = Thm.theory_of_thm th
-      val ctxt = Proof_Context.init_global thy
       val tych = cterm_of thy
       val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
       val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
@@ -101,7 +100,7 @@
                      if (id_thm th) then (So, Si, th::St) else
                      if (solved th) then (th::So, Si, St)
                      else (So, th::Si, St)) nested_tcs ([],[],[])
-              val simplified' = map join_assums simplified
+              val simplified' = map (join_assums ctxt) simplified
               val dummy = (Prim.trace_thms "solved =" solved;
                            Prim.trace_thms "simplified' =" simplified')
               val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
@@ -189,9 +188,9 @@
 fun define_i strict ctxt congs wfs fid R eqs thy =
   let val {functional,pats} = Prim.mk_functional thy eqs
       val (thy, def) = Prim.wfrec_definition0 thy fid R functional
-      val ctxt' = Proof_Context.transfer thy ctxt
+      val ctxt = Proof_Context.transfer thy ctxt
       val (lhs, _) = Logic.dest_equals (prop_of def)
-      val {induct, rules, tcs} = simplify_defn strict thy ctxt' congs wfs fid pats def
+      val {induct, rules, tcs} = simplify_defn strict thy ctxt congs wfs fid pats def
       val rules' = 
           if strict then derive_init_eqs ctxt rules eqs
           else rules
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -432,7 +432,7 @@
        not simplified. Otherwise large examples (Red-Black trees) are too
        slow.*)
      val case_simpset =
-       put_simpset HOL_basic_ss (Proof_Context.init_global theory)
+       put_simpset HOL_basic_ss ctxt
           addsimps case_rewrites
           |> fold (Simplifier.add_cong o #weak_case_cong o snd)
               (Symtab.dest (Datatype.get_all theory))
diff -r 0fd6b0660242 -r 81fff1c65943 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -178,7 +178,7 @@
 fun hol_simplify ctxt rews =
   Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews);
 
-fun unfold_tac ths ctxt =
+fun unfold_tac ctxt ths =
   ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths));
 
 end;
diff -r 0fd6b0660242 -r 81fff1c65943 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Provers/quantifier1.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -68,9 +68,9 @@
   val prove_one_point_ex_tac: tactic
   val rearrange_all: Proof.context -> cterm -> thm option
   val rearrange_ex: Proof.context -> cterm -> thm option
-  val rearrange_ball: tactic -> Proof.context -> cterm -> thm option
-  val rearrange_bex: tactic -> Proof.context -> cterm -> thm option
-  val rearrange_Collect: tactic -> Proof.context -> cterm -> thm option
+  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
 end;
 
 functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -120,12 +120,13 @@
       | exqu xs P = extract (null xs) xs P
   in exqu [] end;
 
-fun prove_conv tac ctxt tu =
+fun prove_conv ctxt tu tac =
   let
     val (goal, ctxt') =
       yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
     val thm =
-      Goal.prove ctxt' [] [] goal (K (rtac Data.iff_reflection 1 THEN tac));
+      Goal.prove ctxt' [] [] goal
+        (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
   in singleton (Variable.export ctxt' ctxt) thm end;
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
@@ -178,7 +179,7 @@
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify all x T xs (Data.imp $ eq $ Q)
-          in SOME (prove_conv prove_one_point_all_tac ctxt (F, R)) end)
+          in SOME (prove_conv ctxt (F, R) (K prove_one_point_all_tac)) end)
   | _ => NONE);
 
 fun rearrange_ball tac ctxt ct =
@@ -190,7 +191,7 @@
           if not (null xs) then NONE
           else
             let val R = Data.imp $ eq $ Q
-            in SOME (prove_conv tac ctxt (F, Ball $ A $ Abs (x, T, R))) end)
+            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
   | _ => NONE);
 
 fun rearrange_ex ctxt ct =
@@ -200,7 +201,7 @@
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify ex x T xs (Data.conj $ eq $ Q)
-          in SOME (prove_conv prove_one_point_ex_tac ctxt (F, R)) end)
+          in SOME (prove_conv ctxt (F, R) (K prove_one_point_ex_tac)) end)
   | _ => NONE);
 
 fun rearrange_bex tac ctxt ct =
@@ -210,7 +211,7 @@
         NONE => NONE
       | SOME (xs, eq, Q) =>
           if not (null xs) then NONE
-          else SOME (prove_conv tac ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))))
+          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
   | _ => NONE);
 
 fun rearrange_Collect tac ctxt ct =
@@ -220,7 +221,7 @@
         NONE => NONE
       | SOME (_, eq, Q) =>
           let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
-          in SOME (prove_conv tac ctxt (F, R)) end)
+          in SOME (prove_conv ctxt (F, R) tac) end)
   | _ => NONE);
 
 end;
diff -r 0fd6b0660242 -r 81fff1c65943 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/Isar/element.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -473,16 +473,18 @@
 
 (* init *)
 
-fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
-  | init (Constrains _) = I
-  | init (Assumes asms) = Context.map_proof (fn ctxt =>
+local
+
+fun init0 (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
+  | init0 (Constrains _) = I
+  | init0 (Assumes asms) = Context.map_proof (fn ctxt =>
       let
         val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
         val (_, ctxt') = ctxt
           |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
           |> Proof_Context.add_assms_i Assumption.assume_export asms';
       in ctxt' end)
-  | init (Defines defs) = Context.map_proof (fn ctxt =>
+  | init0 (Defines defs) = Context.map_proof (fn ctxt =>
       let
         val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
         val asms = defs' |> map (fn (b, (t, ps)) =>
@@ -492,7 +494,17 @@
           |> fold Variable.auto_fixes (map #1 asms)
           |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
       in ctxt' end)
-  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
+  | init0 (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
+
+in
+
+fun init elem context =
+  context
+  |> Context.mapping I Thm.unchecked_hyps
+  |> init0 elem
+  |> Context.mapping I (fn ctxt => Thm.restore_hyps (Context.proof_of context) ctxt);
+
+end;
 
 
 (* activate *)
diff -r 0fd6b0660242 -r 81fff1c65943 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -492,7 +492,7 @@
         handle THM _ => lost_structure ())
       |> Drule.flexflex_unique
       |> Thm.check_shyps (Variable.sorts_of ctxt)
-      |> Thm.check_hyps ctxt;
+      |> Thm.check_hyps (Context.Proof ctxt);
 
     val goal_propss = filter_out null propss;
     val results =
diff -r 0fd6b0660242 -r 81fff1c65943 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/goal.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -168,8 +168,7 @@
 
 fun prove_internal ctxt casms cprop tac =
   (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
-    SOME th => Drule.implies_intr_list casms
-      (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
+    SOME th => Drule.implies_intr_list casms (finish ctxt th)
   | NONE => error "Tactic failed");
 
 
@@ -221,7 +220,7 @@
               (finish ctxt' st
                 |> Drule.flexflex_unique
                 |> Thm.check_shyps sorts
-                (* |> Thm.check_hyps ctxt' *) (* FIXME *))
+                |> Thm.check_hyps (Context.Proof ctxt'))
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
             if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
diff -r 0fd6b0660242 -r 81fff1c65943 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/more_thm.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -54,7 +54,9 @@
   val elim_rules: thm Item_Net.T
   val declare_hyps: cterm -> Proof.context -> Proof.context
   val assume_hyps: cterm -> Proof.context -> thm * Proof.context
-  val check_hyps: Proof.context -> thm -> thm
+  val unchecked_hyps: Proof.context -> Proof.context
+  val restore_hyps: Proof.context -> Proof.context -> Proof.context
+  val check_hyps: Context.generic -> thm -> thm
   val elim_implies: thm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
@@ -266,23 +268,40 @@
 
 structure Hyps = Proof_Data
 (
-  type T = Termtab.set;
-  fun init _ : T = Termtab.empty;
+  type T = Termtab.set * bool;
+  fun init _ : T = (Termtab.empty, true);
 );
 
 fun declare_hyps ct ctxt =
   if Theory.subthy (theory_of_cterm ct, Proof_Context.theory_of ctxt) then
-    Hyps.map (Termtab.update (term_of ct, ())) ctxt
+    (Hyps.map o apfst) (Termtab.update (term_of ct, ())) ctxt
   else raise CTERM ("assume_hyps: bad background theory", [ct]);
 
 fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
 
-fun check_hyps ctxt th =
+val unchecked_hyps = (Hyps.map o apsnd) (K false);
+fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt)));
+
+fun check_hyps context th =
   let
-    val undeclared = filter_out (Termtab.defined (Hyps.get ctxt)) (Thm.hyps_of th);
-    val _ = null undeclared orelse
-      error ("Undeclared hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) undeclared));
-  in th end;
+    val declared_hyps =
+      (case context of
+        Context.Theory _ => K false
+      | Context.Proof ctxt =>
+          (case Hyps.get ctxt of
+            (_, false) => K true
+          | (hyps, _) => Termtab.defined hyps));
+    val undeclared = filter_out declared_hyps (Thm.hyps_of th);
+  in
+    if null undeclared then th
+    else
+      let
+        val ctxt = Context.cases Syntax.init_pretty_global I context;
+      in
+        error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
+          (map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared)))
+      end
+  end;
 
 
 
@@ -434,7 +453,7 @@
 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
 
 fun apply_attribute (att: attribute) th x =
-  let val (x', th') = att (x, Thm.transfer (Context.theory_of x) th)
+  let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
   in (the_default th th', the_default x x') end;
 
 fun attribute_declaration att th x = #2 (apply_attribute att th x);
diff -r 0fd6b0660242 -r 81fff1c65943 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/raw_simplifier.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -70,7 +70,7 @@
 signature RAW_SIMPLIFIER =
 sig
   include BASIC_RAW_SIMPLIFIER
-  exception SIMPLIFIER of string * thm
+  exception SIMPLIFIER of string * thm list
   type trace_ops
   val set_trace_ops: trace_ops -> theory -> theory
   val internal_ss: simpset ->
@@ -114,7 +114,6 @@
   val simp_trace_raw: Config.raw
   val simp_debug_raw: Config.raw
   val add_prems: thm list -> Proof.context -> Proof.context
-  val debug_bounds: bool Unsynchronized.ref
   val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
     Proof.context -> Proof.context
   val set_solvers: solver list -> Proof.context -> Proof.context
@@ -317,14 +316,16 @@
 
 (* empty *)
 
-fun init_ss mk_rews termless subgoal_tac solvers =
-  make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false)),
+fun init_ss bounds depth mk_rews termless subgoal_tac solvers =
+  make_simpset ((Net.empty, [], bounds, depth),
     (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
 
 fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
 
 val empty_ss =
   init_ss
+    (0, [])
+    (0, Unsynchronized.ref false)
     {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
       mk_cong = K I,
       mk_sym = default_mk_sym,
@@ -398,8 +399,8 @@
 fun map_ss f = Context.mapping (map_theory_simpset f) f;
 
 val clear_simpset =
-  map_simpset (fn Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
-    init_ss mk_rews termless subgoal_tac solvers);
+  map_simpset (fn Simpset ({bounds, depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
+    init_ss bounds depth mk_rews termless subgoal_tac solvers);
 
 
 (* simp depth *)
@@ -436,7 +437,7 @@
 
 (* diagnostics *)
 
-exception SIMPLIFIER of string * thm;
+exception SIMPLIFIER of string * thm list;
 
 val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
 val simp_debug = Config.bool simp_debug_raw;
@@ -541,7 +542,7 @@
     val prems = Logic.strip_imp_prems prop;
     val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
     val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
-      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
+      raise SIMPLIFIER ("Rewrite rule not a meta-equality", [thm]);
     val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
     val erhs = Envir.eta_contract (term_of rhs);
     val perm =
@@ -554,7 +555,7 @@
 
 fun decomp_simp' thm =
   let val (_, lhs, _, rhs, _) = decomp_simp thm in
-    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
+    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", [thm])
     else (lhs, rhs)
   end;
 
@@ -666,10 +667,10 @@
   (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
-        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
+        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
     (*val lhs = Envir.eta_contract lhs;*)
       val a = the (cong_name (head_of lhs)) handle Option.Option =>
-        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
+        raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]);
       val (xs, weak) = congs;
       val _ =
         if AList.defined (op =) xs a then
@@ -684,10 +685,10 @@
   (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
-        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
+        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
     (*val lhs = Envir.eta_contract lhs;*)
       val a = the (cong_name (head_of lhs)) handle Option.Option =>
-        raise SIMPLIFIER ("Congruence must start with a constant", thm);
+        raise SIMPLIFIER ("Congruence must start with a constant", [thm]);
       val (xs, _) = congs;
       val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
       val weak' = xs' |> map_filter (fn (a, thm) =>
@@ -1321,27 +1322,6 @@
     prover: how to solve premises in conditional rewrites and congruences
 *)
 
-val debug_bounds = Unsynchronized.ref false;
-
-fun check_bounds ctxt ct =
-  if ! debug_bounds then
-    let
-      val Simpset ({bounds = (_, bounds), ...}, _) = simpset_of ctxt;
-      val bs =
-        fold_aterms
-          (fn Free (x, _) =>
-            if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
-            then insert (op =) x else I
-          | _ => I) (term_of ct) [];
-    in
-      if null bs then ()
-      else
-        print_term ctxt true
-          (fn () => "Simplifier: term contains loose bounds: " ^ commas_quote bs)
-          (Thm.term_of ct)
-    end
-  else ();
-
 fun rewrite_cterm mode prover raw_ctxt raw_ct =
   let
     val thy = Proof_Context.theory_of raw_ctxt;
@@ -1359,7 +1339,6 @@
       |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);
 
     val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
-    val _ = check_bounds ctxt ct;
   in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
 
 val simple_prover =
diff -r 0fd6b0660242 -r 81fff1c65943 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/simplifier.ML	Sun Jan 12 18:42:06 2014 +0100
@@ -31,7 +31,6 @@
   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
   val pretty_simpset: Proof.context -> Pretty.T
   val default_mk_sym: Proof.context -> thm -> thm option
-  val debug_bounds: bool Unsynchronized.ref
   val prems_of: Proof.context -> thm list
   val add_simp: thm -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
diff -r 0fd6b0660242 -r 81fff1c65943 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/ZF/OrdQuant.thy	Sun Jan 12 18:42:06 2014 +0100
@@ -368,17 +368,17 @@
 text {* Setting up the one-point-rule simproc *}
 
 simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {*
-  let
-    val unfold_rex_tac = unfold_tac @{thms rex_def};
-    fun prove_rex_tac ctxt = unfold_rex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
-  in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_rex_tac ctxt) ctxt end
+  fn _ => Quantifier1.rearrange_bex
+    (fn ctxt =>
+      unfold_tac ctxt @{thms rex_def} THEN
+      Quantifier1.prove_one_point_ex_tac)
 *}
 
 simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = {*
-  let
-    val unfold_rall_tac = unfold_tac @{thms rall_def};
-    fun prove_rall_tac ctxt = unfold_rall_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
-  in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_rall_tac ctxt) ctxt end
+  fn _ => Quantifier1.rearrange_ball
+    (fn ctxt =>
+      unfold_tac ctxt @{thms rall_def} THEN
+      Quantifier1.prove_one_point_all_tac)
 *}
 
 end
diff -r 0fd6b0660242 -r 81fff1c65943 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Sat Jan 11 21:03:11 2014 +0100
+++ b/src/ZF/pair.thy	Sun Jan 12 18:42:06 2014 +0100
@@ -19,17 +19,17 @@
 ML {* val ZF_ss = simpset_of @{context} *}
 
 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {*
-  let
-    val unfold_bex_tac = unfold_tac @{thms Bex_def};
-    fun prove_bex_tac ctxt = unfold_bex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
-  in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_bex_tac ctxt) ctxt end
+  fn _ => Quantifier1.rearrange_bex
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Bex_def} THEN
+      Quantifier1.prove_one_point_ex_tac)
 *}
 
 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
-  let
-    val unfold_ball_tac = unfold_tac @{thms Ball_def};
-    fun prove_ball_tac ctxt = unfold_ball_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
-  in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_ball_tac ctxt) ctxt end
+  fn _ => Quantifier1.rearrange_ball
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Ball_def} THEN
+      Quantifier1.prove_one_point_all_tac)
 *}