equal
deleted
inserted
replaced
123 fun mk_insts env = |
123 fun mk_insts env = |
124 (Vartab.dest (Envir.type_env env), |
124 (Vartab.dest (Envir.type_env env), |
125 Envir.alist_of env); |
125 Envir.alist_of env); |
126 val initenv = Envir.Envir {asol = Vartab.empty, |
126 val initenv = Envir.Envir {asol = Vartab.empty, |
127 iTs = typinsttab, maxidx = ix2}; |
127 iTs = typinsttab, maxidx = ix2}; |
128 val useq = (Unify.smash_unifiers (sgn,initenv,[a])) |
128 val useq = Unify.smash_unifiers sgn [a] initenv |
129 handle UnequalLengths => Seq.empty |
129 handle UnequalLengths => Seq.empty |
130 | Term.TERM _ => Seq.empty; |
130 | Term.TERM _ => Seq.empty; |
131 fun clean_unify' useq () = |
131 fun clean_unify' useq () = |
132 (case (Seq.pull useq) of |
132 (case (Seq.pull useq) of |
133 NONE => NONE |
133 NONE => NONE |
378 fun occ_search occ [] = Seq.empty |
378 fun occ_search occ [] = Seq.empty |
379 | occ_search occ ((asminfo, searchinfo)::moreasms) = |
379 | occ_search occ ((asminfo, searchinfo)::moreasms) = |
380 (case searchf searchinfo occ lhs of |
380 (case searchf searchinfo occ lhs of |
381 SkipMore i => occ_search i moreasms |
381 SkipMore i => occ_search i moreasms |
382 | SkipSeq ss => |
382 | SkipSeq ss => |
383 Seq.append (Seq.map (Library.pair asminfo) |
383 Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss)) |
384 (Seq.flat ss), |
384 (occ_search 1 moreasms)) |
385 occ_search 1 moreasms)) |
|
386 (* find later substs also *) |
385 (* find later substs also *) |
387 in |
386 in |
388 occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r) |
387 occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r) |
389 end; |
388 end; |
390 in stepthms |> Seq.maps rewrite_with_thm end; |
389 in stepthms |> Seq.maps rewrite_with_thm end; |