src/HOL/Tools/TFL/post.ML
changeset 55143 04448228381d
parent 54999 7859ed58c041
child 55151 f331472f1027
     1.1 --- a/src/HOL/Tools/TFL/post.ML	Sat Jan 25 21:52:04 2014 +0100
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Jan 25 22:06:07 2014 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4    rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
     1.5  
     1.6  (*Strip off the outer !P*)
     1.7 -val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
     1.8 +val spec'= read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec;
     1.9  
    1.10  fun tracing true _ = ()
    1.11    | tracing false msg = writeln msg;