src/HOL/Tools/TFL/post.ML
changeset 35365 2fcd08c62495
parent 35021 c839a4c670c6
child 35625 9c818cab0dd0
--- a/src/HOL/Tools/TFL/post.ML	Thu Feb 25 22:32:09 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Thu Feb 25 22:46:52 2010 +0100
@@ -125,7 +125,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;
+  Split_Rule.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 =