# HG changeset patch
# User wenzelm
# Date 1385223344 -3600
# Node ID cfe53047dc16e465ac0d819cb649283866f08e2d
# Parent  5f3e9baa8f1375db6943842f3913d3558d8e81a2
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;

diff -r 5f3e9baa8f13 -r cfe53047dc16 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Nov 23 17:07:36 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Nov 23 17:15:44 2013 +0100
@@ -480,28 +480,25 @@
 fun conclude_goal ctxt goal propss =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val string_of_term = Syntax.string_of_term ctxt;
-    val string_of_thm = Display.string_of_thm ctxt;
 
     val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
 
-    val extra_hyps = Assumption.extra_hyps ctxt goal;
-    val _ = null extra_hyps orelse
-      error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
+    fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
 
-    fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
+    val th =
+      (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
+        handle THM _ => lost_structure ())
+      |> Drule.flexflex_unique
+      |> Thm.check_shyps (Variable.sorts_of ctxt)
+      |> Assumption.check_hyps ctxt;
 
-    val th = Goal.conclude
-      (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
-      handle THM _ => lost_structure ();
     val goal_propss = filter_out null propss;
     val results =
       Conjunction.elim_balanced (length goal_propss) th
       |> map2 Conjunction.elim_balanced (map length goal_propss)
       handle THM _ => lost_structure ();
     val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
-      error ("Proved a different theorem:\n" ^ string_of_thm th);
-    val _ = Thm.check_shyps (Variable.sorts_of ctxt) th;
+      error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
 
     fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
       | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
diff -r 5f3e9baa8f13 -r cfe53047dc16 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Sat Nov 23 17:07:36 2013 +0100
+++ b/src/Pure/assumption.ML	Sat Nov 23 17:15:44 2013 +0100
@@ -12,7 +12,7 @@
   val assume: cterm -> thm
   val all_assms_of: Proof.context -> cterm list
   val all_prems_of: Proof.context -> thm list
-  val extra_hyps: Proof.context -> thm -> term list
+  val check_hyps: Proof.context -> thm -> thm
   val local_assms_of: Proof.context -> Proof.context -> cterm list
   val local_prems_of: Proof.context -> Proof.context -> thm list
   val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
@@ -76,8 +76,12 @@
 val all_assms_of = maps #2 o all_assumptions_of;
 val all_prems_of = #prems o rep_data;
 
-fun extra_hyps ctxt th =
-  subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
+fun check_hyps ctxt th =
+  let
+    val extra_hyps = subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
+    val _ = null extra_hyps orelse
+      error ("Additional hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) extra_hyps));
+  in th end;
 
 
 (* local assumptions *)
diff -r 5f3e9baa8f13 -r cfe53047dc16 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Nov 23 17:07:36 2013 +0100
+++ b/src/Pure/goal.ML	Sat Nov 23 17:15:44 2013 +0100
@@ -182,7 +182,6 @@
 fun prove_common immediate pri ctxt xs asms props tac =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val string_of_term = Syntax.string_of_term ctxt;
 
     val schematic = exists is_schematic props;
     val future = future_enabled 1;
@@ -191,7 +190,7 @@
     val pos = Position.thread_data ();
     fun err msg = cat_error msg
       ("The error(s) above occurred for the goal statement:\n" ^
-        string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
+        Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
         (case Position.here pos of "" => "" | s => "\n" ^ s));
 
     fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
@@ -215,10 +214,16 @@
       (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of
         NONE => err "Tactic failed"
       | SOME st =>
-          let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
-            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
-            then Thm.check_shyps sorts res
-            else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
+          let
+            val res =
+              (finish ctxt' st
+                |> Drule.flexflex_unique
+                |> Thm.check_shyps sorts
+                (* |> Assumption.check_hyps 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
+            else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
           end);
     val res =
       if immediate orelse schematic orelse not future orelse skip then result ()