# HG changeset patch
# User wenzelm
# Date 1434405400 -7200
# Node ID 2803bc16742c43cf34592ca380ecd7293e3963f8
# Parent  2abfcf85c62728dccde5a80ce5ac3822d4100976# Parent  9b28f446d9c520688ab52cdf20b05a4d9a4826a7
merged

diff -r 2abfcf85c627 -r 2803bc16742c NEWS
--- a/NEWS	Mon Jun 15 21:33:26 2015 +0100
+++ b/NEWS	Mon Jun 15 23:56:40 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 2abfcf85c627 -r 2803bc16742c src/HOL/Tools/functor.ML
--- a/src/HOL/Tools/functor.ML	Mon Jun 15 21:33:26 2015 +0100
+++ b/src/HOL/Tools/functor.ML	Mon Jun 15 23:56:40 2015 +0200
@@ -9,7 +9,7 @@
   val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list
   val construct_mapper: Proof.context -> (string * bool -> term)
     -> bool -> typ -> typ -> term
-  val functorx: string option -> term -> local_theory -> Proof.state
+  val functor_: string option -> term -> local_theory -> Proof.state
   val functor_cmd: string option -> string -> Proof.context -> Proof.state
   type entry
   val entries: Proof.context -> entry list Symtab.table
@@ -269,7 +269,7 @@
     |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
   end
 
-val functorx = gen_functor Syntax.check_term;
+val functor_ = gen_functor Syntax.check_term;
 val functor_cmd = gen_functor Syntax.read_term;
 
 val _ =
diff -r 2abfcf85c627 -r 2803bc16742c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jun 15 21:33:26 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Jun 15 23:56:40 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);
 
diff -r 2abfcf85c627 -r 2803bc16742c src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Jun 15 21:33:26 2015 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Jun 15 23:56:40 2015 +0200
@@ -399,8 +399,9 @@
           val limit = Config.get ctxt Syntax.ambiguity_limit;
 
           (*brute-force disambiguation via type-inference*)
-          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
-            handle exn as ERROR _ => Exn.Exn exn;
+          fun check t =
+            (Syntax.check_term (Proof_Context.allow_dummies ctxt) (constrain t); Exn.Res t)
+              handle exn as ERROR _ => Exn.Exn exn;
 
           val results' =
             if parsed_len > 1 then