src/FOLP/ROOT.ML

    (fn prems => [ REPEAT(resolve_tac prems 1) ]);
 
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
+  val thin_refl = prove_goal IFOLP.thy 
+		  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
   end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;