src/Pure/thm.ML
changeset 7528 ee5f37e4f186
parent 7323 16b7e2f1b4e3
child 7534 30344dde83ab
equal deleted inserted replaced
7527:9e2dddd8b81f 7528:ee5f37e4f186
  1503              Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
  1503              Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
  1504                        (Seq.make (fn()=> cell), Seq.empty)
  1504                        (Seq.make (fn()=> cell), Seq.empty)
  1505  in  if eres_flg then eres(rev rAs)
  1505  in  if eres_flg then eres(rev rAs)
  1506      else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
  1506      else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
  1507  end;
  1507  end;
  1508 end;  (*open Sequence*)
  1508 end;
  1509 
  1509 
  1510 
  1510 
  1511 fun bicompose match arg i state =
  1511 fun bicompose match arg i state =
  1512     bicompose_aux match (state, dest_state(state,i), false) arg;
  1512     bicompose_aux match (state, dest_state(state,i), false) arg;
  1513 
  1513