# HG changeset patch
# User wenzelm
# Date 981148866 -3600
# Node ID 932d66879fe797fab6ebe4f59724a3c813fdacd9
# Parent  37716a82a3d9a50eb278b97a9ab99f73afcc4d04
tuned;

diff -r 37716a82a3d9 -r 932d66879fe7 TFL/post.ML
--- a/TFL/post.ML	Fri Feb 02 22:20:43 2001 +0100
+++ b/TFL/post.ML	Fri Feb 02 22:21:06 2001 +0100
@@ -153,16 +153,13 @@
 
 
 (*lcp: curry the predicate of the induction rule*)
-fun curry_rule rl = split_rule_var
-                        (head_of (HOLogic.dest_Trueprop (concl_of rl)),
-                         rl);
+fun curry_rule 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 =
-    curry_rule o standard o
-    rule_by_tactic (REPEAT
-                    (FIRSTGOAL (resolve_tac [allI, impI, conjI]
-                                ORELSE' etac conjE)));
+  curry_rule o standard o
+  rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
 
 (*Strip off the outer !P*)
 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;