src/HOL/Tools/split_rule.ML

--- a/src/HOL/Tools/split_rule.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/split_rule.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -89,7 +89,7 @@
 
 (*curries ALL function variables occurring in a rule's conclusion*)
 fun split_rule ctxt rl =
-  fold_rev split_rule_var' (Misc_Legacy.term_vars (concl_of rl)) rl
+  fold_rev split_rule_var' (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
   |> remove_internal_split ctxt
   |> Drule.export_without_context;