# HG changeset patch
# User wenzelm
# Date 1434380367 -7200
# Node ID bfd9b7302a82289642b861551a18eae533322f81
# Parent  fa31b5d36bebaa7612b48eb79050993dea916e56
vacuous fact `TERM x`;

diff -r fa31b5d36beb -r bfd9b7302a82 NEWS
--- a/NEWS	Mon Jun 15 16:24:52 2015 +0200
+++ b/NEWS	Mon Jun 15 16:59:27 2015 +0200
@@ -65,6 +65,9 @@
 
 *** Pure ***
 
+* The vacuous fact "TERM x" may be established "by fact" or as `TERM x`
+as well, not just "by this" or "." as before.
+
 * Configuration option rule_insts_schematic has been discontinued
 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
 
diff -r fa31b5d36beb -r bfd9b7302a82 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jun 15 16:24:52 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jun 15 16:59:27 2015 +0200
@@ -909,12 +909,17 @@
       (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND
       comp_incr_tac ctxt ths i;
 
+val vacuous_facts = [Drule.termI];
+
 in
 
 fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
 
 fun potential_facts ctxt prop =
-  Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
+  let
+    val body = Term.strip_all_body prop;
+    val vacuous = filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts;
+  in Facts.could_unify (facts_of ctxt) body @ vacuous end;
 
 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i);