--- 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;
--- 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
--- 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;