src/Provers/splitter.ML
changeset 29548 02a52ae34b7a
parent 28839 32d498cf7595
child 30510 4120fc59dd85
equal deleted inserted replaced
29529:70ef35ccdc3b 29548:02a52ae34b7a
   144    tt    : the term  Const(key,..) $ ...
   144    tt    : the term  Const(key,..) $ ...
   145 *************************************************************************)
   145 *************************************************************************)
   146 
   146 
   147 fun mk_cntxt_splitthm t tt T =
   147 fun mk_cntxt_splitthm t tt T =
   148   let fun repl lev t =
   148   let fun repl lev t =
   149     if incr_boundvars lev tt aconv t then Bound lev
   149     if Pattern.aeconv(incr_boundvars lev tt, t) then Bound lev
   150     else case t of
   150     else case t of
   151         (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
   151         (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
   152       | (Bound i) => Bound (if i>=lev then i+1 else i)
   152       | (Bound i) => Bound (if i>=lev then i+1 else i)
   153       | (t1 $ t2) => (repl lev t1) $ (repl lev t2)
   153       | (t1 $ t2) => (repl lev t1) $ (repl lev t2)
   154       | t => t
   154       | t => t