src/HOL/Library/rewrite.ML
changeset 60052 616a17640229
parent 60051 2a1cab4c9c9d
child 60053 0e9895ffab1d
     1.1 --- a/src/HOL/Library/rewrite.ML	Mon Apr 13 14:45:44 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 14:52:40 2015 +0200
     1.3 @@ -253,14 +253,16 @@
     1.4              | SOME ft => SOME ft
     1.5        in desc eta_expands ft end
     1.6  
     1.7 -    fun seq_unfold f ft =
     1.8 -      case f ft of
     1.9 -        NONE => Seq.empty
    1.10 -      | SOME ft' => Seq.cons ft' (seq_unfold f ft')
    1.11 +    fun move_assms ctxt (ft: focusterm) =
    1.12 +      let
    1.13 +        fun f () = case try (ft_assm ctxt) ft of
    1.14 +            NONE => NONE
    1.15 +          | SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft))
    1.16 +      in Seq.make f end
    1.17  
    1.18      fun apply_pat At = Seq.map (ft_judgment ctxt)
    1.19        | apply_pat In = Seq.maps (valid_match_points ctxt)
    1.20 -      | apply_pat Asm = Seq.maps (seq_unfold (try (ft_assm ctxt)) o ft_params ctxt)
    1.21 +      | apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt)
    1.22        | apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt)
    1.23        | apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents)))
    1.24        | apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x))