TFL/post.ML

--- a/TFL/post.ML	Sat May 27 17:42:00 2006 +0200
+++ b/TFL/post.ML	Sat May 27 17:42:02 2006 +0200
@@ -156,7 +156,7 @@
 
 (*lcp: curry the predicate of the induction rule*)
 fun curry_rule rl =
-  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl)), rl);
+  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
 
 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
 val meta_outer =