src/HOL/Tools/TFL/post.ML

--- a/src/HOL/Tools/TFL/post.ML	Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Sat Jan 25 22:06:07 2014 +0100
@@ -130,7 +130,7 @@
   rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
 
 (*Strip off the outer !P*)
-val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
+val spec'= read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec;
 
 fun tracing true _ = ()
   | tracing false msg = writeln msg;