# HG changeset patch
# User wenzelm
# Date 1389467191 -3600
# Node ID 625370769fc0784999868f96a92b8272324e1b7c
# Parent  e5f4075d4c5e1c14fbd0226a6abd490e9d753939
check_hyps for attribute application (still inactive, due to non-compliant tools);
bypass check_hyps for locale expressions, where assumptions are not necessarily declared in intermediate situations;

diff -r e5f4075d4c5e -r 625370769fc0 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Jan 11 17:05:03 2014 +0100
+++ b/src/Pure/Isar/element.ML	Sat Jan 11 20:06:31 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 e5f4075d4c5e -r 625370769fc0 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Jan 11 17:05:03 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Jan 11 20:06:31 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 e5f4075d4c5e -r 625370769fc0 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Jan 11 17:05:03 2014 +0100
+++ b/src/Pure/goal.ML	Sat Jan 11 20:06:31 2014 +0100
@@ -220,7 +220,7 @@
               (finish ctxt' st
                 |> Drule.flexflex_unique
                 |> Thm.check_shyps sorts
-                (* |> Thm.check_hyps ctxt' *) (* FIXME *))
+                (* |> Thm.check_hyps (Context.Proof ctxt') *) (* FIXME *))
               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 e5f4075d4c5e -r 625370769fc0 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Jan 11 17:05:03 2014 +0100
+++ b/src/Pure/more_thm.ML	Sat Jan 11 20:06:31 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 *) (* FIXME *) (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);