tuned;
authorwenzelm
Fri Feb 02 22:21:06 2001 +0100 (2001-02-02)
changeset 11038932d66879fe7
parent 11037 37716a82a3d9
child 11039 55de839f4850
tuned;
TFL/post.ML
     1.1 --- a/TFL/post.ML	Fri Feb 02 22:20:43 2001 +0100
     1.2 +++ b/TFL/post.ML	Fri Feb 02 22:21:06 2001 +0100
     1.3 @@ -153,16 +153,13 @@
     1.4  
     1.5  
     1.6  (*lcp: curry the predicate of the induction rule*)
     1.7 -fun curry_rule rl = split_rule_var
     1.8 -                        (head_of (HOLogic.dest_Trueprop (concl_of rl)),
     1.9 -                         rl);
    1.10 +fun curry_rule rl =
    1.11 +  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl)), rl);
    1.12  
    1.13  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
    1.14  val meta_outer =
    1.15 -    curry_rule o standard o
    1.16 -    rule_by_tactic (REPEAT
    1.17 -                    (FIRSTGOAL (resolve_tac [allI, impI, conjI]
    1.18 -                                ORELSE' etac conjE)));
    1.19 +  curry_rule o standard o
    1.20 +  rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
    1.21  
    1.22  (*Strip off the outer !P*)
    1.23  val spec'= read_instantiate [("x","P::?'b=>bool")] spec;