src/HOL/Library/rewrite.ML
changeset 60050 dc6ac152d864
parent 59975 da10875adf8e
child 60051 2a1cab4c9c9d
     1.1 --- a/src/HOL/Library/rewrite.ML	Mon Apr 13 11:58:18 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 12:18:47 2015 +0200
     1.3 @@ -76,6 +76,7 @@
     1.4  
     1.5  val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
     1.6  val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
     1.7 +val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr
     1.8  
     1.9  
    1.10  (* focus terms *)
    1.11 @@ -102,9 +103,18 @@
    1.12    | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
    1.13    | ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t])
    1.14  
    1.15 -fun ft_arg _ (tyenv, _ $ r, pos) = (tyenv, r, pos o arg_rewr_cconv)
    1.16 -  | ft_arg ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg ctxt o ft_abs ctxt (NONE, T)) ft
    1.17 -  | ft_arg _ (_, t, _) = raise TERM ("ft_arg", [t])
    1.18 +local
    1.19 +
    1.20 +fun ft_arg_gen cconv _ (tyenv, _ $ r, pos) = (tyenv, r, pos o cconv)
    1.21 +  | ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft
    1.22 +  | ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t])
    1.23 +
    1.24 +in
    1.25 +
    1.26 +val ft_arg = ft_arg_gen arg_rewr_cconv
    1.27 +val ft_imp = ft_arg_gen imp_rewr_cconv
    1.28 +
    1.29 +end
    1.30  
    1.31  (* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
    1.32  fun ft_params ctxt (ft as (_, t, _) : focusterm) =
    1.33 @@ -141,7 +151,7 @@
    1.34  
    1.35  fun ft_concl ctxt (ft as (_, t, _) : focusterm) =
    1.36    case t of
    1.37 -    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt) ft
    1.38 +    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft
    1.39    | _ => ft
    1.40  
    1.41  fun ft_assm ctxt (ft as (_, t, _) : focusterm) =