src/HOL/Library/rewrite.ML
changeset 60054 ef4878146485
parent 60053 0e9895ffab1d
child 60055 aa3d2a6dd99e
     1.1 --- a/src/HOL/Library/rewrite.ML	Mon Apr 13 15:32:32 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 20:11:12 2015 +0200
     1.3 @@ -77,6 +77,7 @@
     1.4  val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
     1.5  val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
     1.6  val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr
     1.7 +val with_prems_rewr_cconv : subterm_position = fn rewr => CConv.with_prems_cconv ~1 oo rewr
     1.8  
     1.9  
    1.10  (* focus terms *)
    1.11 @@ -154,10 +155,9 @@
    1.12      (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft
    1.13    | _ => ft
    1.14  
    1.15 -fun ft_assm ctxt (ft as (_, t, _) : focusterm) =
    1.16 -  case t of
    1.17 -    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_arg ctxt o ft_fun ctxt) ft
    1.18 -  | _ => raise TERM ("ft_assm", [t])
    1.19 +fun ft_assm _ (tyenv, (Const (@{const_name "Pure.imp"}, _) $ l) $ _, pos) =
    1.20 +      (tyenv, l, pos o with_prems_rewr_cconv)
    1.21 +  | ft_assm _ (_, t, _) = raise TERM ("ft_assm", [t])
    1.22  
    1.23  fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
    1.24    if Object_Logic.is_judgment ctxt t