src/HOL/Tools/TFL/post.ML

--- a/src/HOL/Tools/TFL/post.ML	Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Mon Jun 16 22:13:39 2008 +0200
@@ -152,7 +152,7 @@
   rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
 
 (*Strip off the outer !P*)
-val spec'= RuleInsts.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;