changeset 60053 | 0e9895ffab1d |
parent 60052 | 616a17640229 |
child 60054 | ef4878146485 |
--- a/src/HOL/Library/rewrite.ML Mon Apr 13 14:52:40 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Mon Apr 13 15:32:32 2015 +0200 @@ -156,7 +156,7 @@ fun ft_assm ctxt (ft as (_, t, _) : focusterm) = case t of - (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt o ft_fun ctxt) ft + (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_arg ctxt o ft_fun ctxt) ft | _ => raise TERM ("ft_assm", [t]) fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =