--- a/src/Pure/display.ML Thu Feb 20 20:19:41 2014 +0100
+++ b/src/Pure/display.ML Thu Feb 20 20:59:15 2014 +0100
@@ -55,22 +55,21 @@
val th = Thm.strip_shyps raw_th;
val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
- val xshyps = Thm.extra_shyps th;
+ val hyps' = if show_hyps then hyps else Thm.undeclared_hyps (Context.Proof ctxt) th;
+ val extra_shyps = Thm.extra_shyps th;
val tags = Thm.get_tags th;
val q = if quote then Pretty.quote else I;
val prt_term = q o Syntax.pretty_term ctxt;
- val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
- val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps;
- val hlen = length xshyps + length hyps' + length tpairs;
+ val hlen = length extra_shyps + length hyps' + length tpairs;
val hsymbs =
if hlen = 0 then []
else if show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
(map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
- map (Syntax.pretty_sort ctxt) xshyps)]
+ map (Syntax.pretty_sort ctxt) extra_shyps)]
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
val tsymbs =
if null tags orelse not show_tags then []
--- a/src/Pure/more_thm.ML Thu Feb 20 20:19:41 2014 +0100
+++ b/src/Pure/more_thm.ML Thu Feb 20 20:59:15 2014 +0100
@@ -55,6 +55,7 @@
val assume_hyps: cterm -> Proof.context -> thm * Proof.context
val unchecked_hyps: Proof.context -> Proof.context
val restore_hyps: Proof.context -> Proof.context -> Proof.context
+ val undeclared_hyps: Context.generic -> thm -> term list
val check_hyps: Context.generic -> thm -> thm
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
@@ -281,26 +282,26 @@
val unchecked_hyps = (Hyps.map o apsnd) (K false);
fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt)));
+fun undeclared_hyps context th =
+ Thm.hyps_of th
+ |> filter_out
+ (case context of
+ Context.Theory _ => K false
+ | Context.Proof ctxt =>
+ (case Hyps.get ctxt of
+ (_, false) => K true
+ | (hyps, _) => Termtab.defined hyps));
+
fun check_hyps context th =
- let
- 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
+ (case undeclared_hyps context th of
+ [] => th
+ | undeclared =>
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;
+ end);