src/HOL/Tools/TFL/post.ML
changeset 55151 f331472f1027
parent 55143 04448228381d
child 55236 8d61b0aa7a0d
     1.1 --- a/src/HOL/Tools/TFL/post.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Sun Jan 26 13:45:40 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'= Rule_Insts.read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec;
     1.9  
    1.10  fun tracing true _ = ()
    1.11    | tracing false msg = writeln msg;