# HG changeset patch
# User wenzelm
# Date 1438106753 -7200
# Node ID e1f1842bf344baa557c47459e48b09ae872b2d79
# Parent  5e11a6e2b044cb634fe3adb1f98ca0605d165f22
proper context;

diff -r 5e11a6e2b044 -r e1f1842bf344 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jul 28 19:49:54 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 28 20:05:53 2015 +0200
@@ -501,7 +501,7 @@
       (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
         handle THM _ => err_lost ())
       |> Drule.flexflex_unique (SOME ctxt)
-      |> Thm.check_shyps (Variable.sorts_of ctxt)
+      |> Thm.check_shyps ctxt (Variable.sorts_of ctxt)
       |> Thm.check_hyps (Context.Proof ctxt);
 
     val goal_propss = filter_out null propss;
diff -r 5e11a6e2b044 -r e1f1842bf344 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Jul 28 19:49:54 2015 +0200
+++ b/src/Pure/goal.ML	Tue Jul 28 20:05:53 2015 +0200
@@ -214,7 +214,7 @@
             val res =
               (finish ctxt' st
                 |> Drule.flexflex_unique (SOME ctxt')
-                |> Thm.check_shyps sorts
+                |> Thm.check_shyps ctxt' sorts
                 |> Thm.check_hyps (Context.Proof ctxt'))
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
diff -r 5e11a6e2b044 -r e1f1842bf344 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 28 19:49:54 2015 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 28 20:05:53 2015 +0200
@@ -43,7 +43,7 @@
   val equiv_thm: theory -> thm * thm -> bool
   val class_triv: theory -> class -> thm
   val of_sort: ctyp * sort -> thm list
-  val check_shyps: sort list -> thm -> thm
+  val check_shyps: Proof.context -> sort list -> thm -> thm
   val is_dummy: thm -> bool
   val plain_prop_of: thm -> term
   val add_thm: thm -> thm list -> thm list
@@ -216,15 +216,14 @@
 
 fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
 
-fun check_shyps sorts raw_th =
+fun check_shyps ctxt sorts raw_th =
   let
     val th = Thm.strip_shyps raw_th;
-    val prt_sort = Syntax.pretty_sort_global (Thm.theory_of_thm th);
     val pending = Sorts.subtract sorts (Thm.extra_shyps th);
   in
     if null pending then th
     else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
-      Pretty.brk 1 :: Pretty.commas (map prt_sort pending))))
+      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
   end;