src/Provers/splitter.ML
changeset 3537 79ac9b475621
parent 2266 82aef6857c5b
child 3835 9a5a4e123859
     1.1 --- a/src/Provers/splitter.ML	Fri Jul 18 14:06:54 1997 +0200
     1.2 +++ b/src/Provers/splitter.ML	Tue Jul 22 11:12:55 1997 +0200
     1.3 @@ -261,21 +261,21 @@
     1.4                             val (Const(a,_),args) = strip_comb lhs
     1.5                         in (a,(thm,fastype_of t,length args)) end
     1.6        val cmap = map const splits;
     1.7 -      fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i
     1.8 -      fun lift_split state =
     1.9 -            let val (Ts,t,splits) = select cmap state i
    1.10 +      fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st
    1.11 +      fun lift_split_tac st = st |>
    1.12 +            let val (Ts,t,splits) = select cmap st i
    1.13              in case splits of
    1.14                   [] => no_tac
    1.15                 | (thm,apsns,pos,TB,tt)::_ =>
    1.16                     (case apsns of
    1.17 -                      [] => STATE(fn state => rtac (inst_split Ts t tt thm TB state) i)
    1.18 -                    | p::_ => EVERY[STATE(lift Ts t p),
    1.19 +                      [] => (fn state => state |>
    1.20 +			           rtac (inst_split Ts t tt thm TB state) i)
    1.21 +                    | p::_ => EVERY[lift_tac Ts t p,
    1.22                                      rtac reflexive_thm (i+1),
    1.23 -                                    STATE lift_split])
    1.24 +                                    lift_split_tac])
    1.25              end
    1.26 -  in STATE(fn thm =>
    1.27 -       if i <= nprems_of thm then rtac iffD i THEN STATE lift_split
    1.28 -       else no_tac)
    1.29 +  in COND (has_fewer_prems i) no_tac 
    1.30 +          (rtac iffD i THEN lift_split_tac)
    1.31    end;
    1.32  
    1.33  in split_tac end;