src/Pure/thm.ML
changeset 4270 957c887b89b5
parent 4254 8ae7ace96c39
child 4281 6c6073b13600
     1.1 --- a/src/Pure/thm.ML	Fri Nov 21 15:26:22 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Nov 21 15:27:43 1997 +0100
     1.3 @@ -19,8 +19,7 @@
     1.4    (*certified terms*)
     1.5    type cterm
     1.6    exception CTERM of string
     1.7 -  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ,
     1.8 -                                    maxidx: int}
     1.9 +  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
    1.10    val term_of           : cterm -> term
    1.11    val cterm_of          : Sign.sg -> term -> cterm
    1.12    val ctyp_of_term      : cterm -> ctyp
    1.13 @@ -121,7 +120,7 @@
    1.14    val equal_intr        : thm -> thm -> thm
    1.15    val equal_elim        : thm -> thm -> thm
    1.16    val implies_intr_hyps : thm -> thm
    1.17 -  val flexflex_rule     : thm -> thm Sequence.seq
    1.18 +  val flexflex_rule     : thm -> thm Seq.seq
    1.19    val instantiate       :
    1.20      (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
    1.21    val trivial           : cterm -> thm
    1.22 @@ -131,14 +130,14 @@
    1.23    val dest_state        : thm * int ->
    1.24      (term * term) list * term list * term * term
    1.25    val lift_rule         : (thm * int) -> thm -> thm
    1.26 -  val assumption        : int -> thm -> thm Sequence.seq
    1.27 +  val assumption        : int -> thm -> thm Seq.seq
    1.28    val eq_assumption     : int -> thm -> thm
    1.29    val rotate_rule       : int -> int -> thm -> thm
    1.30    val rename_params_rule: string list * int -> thm -> thm
    1.31    val bicompose         : bool -> bool * thm * int ->
    1.32 -    int -> thm -> thm Sequence.seq
    1.33 +    int -> thm -> thm Seq.seq
    1.34    val biresolution      : bool -> (bool * thm) list ->
    1.35 -    int -> thm -> thm Sequence.seq
    1.36 +    int -> thm -> thm Seq.seq
    1.37  
    1.38    (*meta simplification*)
    1.39    exception SIMPLIFIER of string * thm
    1.40 @@ -1016,7 +1015,7 @@
    1.41                       prop = newprop})
    1.42            end;
    1.43        val (tpairs,_) = Logic.strip_flexpairs prop
    1.44 -  in Sequence.maps newthm
    1.45 +  in Seq.map newthm
    1.46              (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
    1.47    end;
    1.48  
    1.49 @@ -1181,9 +1180,9 @@
    1.50                     Logic.rule_of (tpairs, Bs, C)
    1.51                 else (*normalize the new rule fully*)
    1.52                     Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
    1.53 -      fun addprfs [] = Sequence.null
    1.54 -        | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
    1.55 -             (Sequence.mapp newth
    1.56 +      fun addprfs [] = Seq.empty
    1.57 +        | addprfs ((t,u)::apairs) = Seq.make (fn()=> Seq.pull
    1.58 +             (Seq.mapp newth
    1.59                  (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
    1.60                  (addprfs apairs)))
    1.61    in  addprfs (Logic.assum_pairs Bi)  end;
    1.62 @@ -1349,7 +1348,7 @@
    1.63    nsubgoal is the number of new subgoals (written m above).
    1.64    Curried so that resolution calls dest_state only once.
    1.65  *)
    1.66 -local open Sequence; exception COMPOSE
    1.67 +local exception COMPOSE
    1.68  in
    1.69  fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
    1.70                          (eres_flg, orule, nsubgoal) =
    1.71 @@ -1387,7 +1386,7 @@
    1.72                   shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
    1.73                   hyps = union_term(rhyps,shyps),
    1.74                   prop = Logic.rule_of normp}
    1.75 -        in  cons(th, thq)  end  handle COMPOSE => thq
    1.76 +        in  Seq.cons(th, thq)  end  handle COMPOSE => thq
    1.77       val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
    1.78       val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
    1.79         handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
    1.80 @@ -1403,23 +1402,23 @@
    1.81       val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
    1.82       val dpairs = BBi :: (rtpairs@stpairs);
    1.83       (*elim-resolution: try each assumption in turn.  Initially n=1*)
    1.84 -     fun tryasms (_, _, []) = null
    1.85 +     fun tryasms (_, _, []) = Seq.empty
    1.86         | tryasms (As, n, (t,u)::apairs) =
    1.87 -          (case pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
    1.88 +          (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
    1.89                 None                   => tryasms (As, n+1, apairs)
    1.90               | cell as Some((_,tpairs),_) =>
    1.91 -                   its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
    1.92 -                       (seqof (fn()=> cell),
    1.93 -                        seqof (fn()=> pull (tryasms (As, n+1, apairs)))));
    1.94 +                   Seq.it_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
    1.95 +                       (Seq.make (fn()=> cell),
    1.96 +                        Seq.make (fn()=> Seq.pull (tryasms (As, n+1, apairs)))));
    1.97       fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
    1.98         | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
    1.99       (*ordinary resolution*)
   1.100 -     fun res(None) = null
   1.101 +     fun res(None) = Seq.empty
   1.102         | res(cell as Some((_,tpairs),_)) =
   1.103 -             its_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
   1.104 -                       (seqof (fn()=> cell), null)
   1.105 +             Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
   1.106 +                       (Seq.make (fn()=> cell), Seq.empty)
   1.107   in  if eres_flg then eres(rev rAs)
   1.108 -     else res(pull(Unify.unifiers(sign, env, dpairs)))
   1.109 +     else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
   1.110   end;
   1.111  end;  (*open Sequence*)
   1.112  
   1.113 @@ -1444,14 +1443,14 @@
   1.114          val B = Logic.strip_assums_concl Bi;
   1.115          val Hs = Logic.strip_assums_hyp Bi;
   1.116          val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
   1.117 -        fun res [] = Sequence.null
   1.118 +        fun res [] = Seq.empty
   1.119            | res ((eres_flg, rule)::brules) =
   1.120                if could_bires (Hs, B, eres_flg, rule)
   1.121 -              then Sequence.seqof (*delay processing remainder till needed*)
   1.122 +              then Seq.make (*delay processing remainder till needed*)
   1.123                    (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
   1.124                                 res brules))
   1.125                else res brules
   1.126 -    in  Sequence.flats (res brules)  end;
   1.127 +    in  Seq.flat (res brules)  end;
   1.128  
   1.129  
   1.130