# HG changeset patch
# User wenzelm
# Date 1248606772 -7200
# Node ID bc341bbe4417ebbfaa2e9080e90342ea2f920ebe
# Parent  bda40fb76a65ef21b35f20fe7779ee1db2f005d2
Goal.finish: explicit context for printing;

diff -r bda40fb76a65 -r bc341bbe4417 src/HOL/SizeChange/sct.ML
--- a/src/HOL/SizeChange/sct.ML	Sat Jul 25 18:55:30 2009 +0200
+++ b/src/HOL/SizeChange/sct.ML	Sun Jul 26 13:12:52 2009 +0200
@@ -210,7 +210,7 @@
 
     in
       if Thm.no_prems no_step
-      then NoStep (Goal.finish no_step RS no_stepI)
+      then NoStep (Goal.finish ctxt no_step RS no_stepI)
       else
         let
           fun set_m1 i =
@@ -240,10 +240,10 @@
                       val thm1 = decr with_m2
                     in
                       if Thm.no_prems thm1
-                      then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1))
+                      then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish ctxt thm1) 1))
                       else let val thm2 = decreq with_m2 in
                              if Thm.no_prems thm2
-                             then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1))
+                             then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish ctxt thm2) 1))
                              else all_tac end
                     end
               in set_m2 end
@@ -257,7 +257,7 @@
                     |> cterm_of thy
                     |> Goal.init
                     |> tac |> Seq.hd
-                    |> Goal.finish
+                    |> Goal.finish ctxt
 
           val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
         in
diff -r bda40fb76a65 -r bc341bbe4417 src/HOL/Tools/Function/fundef_lib.ML
--- a/src/HOL/Tools/Function/fundef_lib.ML	Sat Jul 25 18:55:30 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_lib.ML	Sun Jul 26 13:12:52 2009 +0200
@@ -126,7 +126,10 @@
 fun try_proof cgoal tac = 
     case SINGLE tac (Goal.init cgoal) of
       NONE => Fail
-    | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
+    | SOME st =>
+        if Thm.no_prems st
+        then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
+        else Stuck st
 
 
 fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = 
diff -r bda40fb76a65 -r bc341bbe4417 src/HOL/Tools/Function/induction_scheme.ML
--- a/src/HOL/Tools/Function/induction_scheme.ML	Sat Jul 25 18:55:30 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Sun Jul 26 13:12:52 2009 +0200
@@ -324,7 +324,7 @@
                          THEN CONVERSION ind_rulify 1)
                      |> Seq.hd
                      |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
-                     |> Goal.finish
+                     |> Goal.finish ctxt
                      |> implies_intr (cprop_of branch_hyp)
                      |> fold_rev (forall_intr o cert) fxs
           in
diff -r bda40fb76a65 -r bc341bbe4417 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Jul 25 18:55:30 2009 +0200
+++ b/src/Pure/axclass.ML	Sun Jul 26 13:12:52 2009 +0200
@@ -607,8 +607,10 @@
     val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
     val ths =
       sort |> map (fn c =>
-        Goal.finish (the (lookup_type cache' typ c) RS
-          Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
+        Goal.finish
+          (Syntax.init_pretty_global thy)
+          (the (lookup_type cache' typ c) RS
+            Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
         |> Thm.adjust_maxidx_thm ~1);
   in (ths, cache') end;
 
diff -r bda40fb76a65 -r bc341bbe4417 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Jul 25 18:55:30 2009 +0200
+++ b/src/Pure/goal.ML	Sun Jul 26 13:12:52 2009 +0200
@@ -18,7 +18,8 @@
   val init: cterm -> thm
   val protect: thm -> thm
   val conclude: thm -> thm
-  val finish: thm -> thm
+  val check_finished: Proof.context -> thm -> unit
+  val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
   val future_enabled: unit -> bool
   val local_future_enabled: unit -> bool
@@ -74,12 +75,15 @@
   --- (finish)
    C
 *)
-fun finish th =
+fun check_finished ctxt th =
   (case Thm.nprems_of th of
-    0 => conclude th
+    0 => ()
   | n => raise THM ("Proof failed.\n" ^
-      Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context n th)) ^
-      ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
+      Pretty.string_of (Pretty.chunks
+        (Goal_Display.pretty_goals ctxt {total = true, main = true, maxgoals = n} th)) ^
+      "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
+
+fun finish ctxt th = (check_finished ctxt th; conclude th);
 
 
 
@@ -145,7 +149,8 @@
 
 fun prove_internal casms cprop tac =
   (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
-    SOME th => Drule.implies_intr_list casms (finish th)
+    SOME th => Drule.implies_intr_list casms
+      (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
   | NONE => error "Tactic failed.");
 
 
@@ -180,7 +185,7 @@
       (case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
         NONE => err "Tactic failed."
       | SOME st =>
-          let val res = finish st handle THM (msg, _, _) => err msg in
+          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))