--- 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) =
--- a/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 14:52:40 2015 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 15:32:32 2015 +0200
@@ -88,6 +88,14 @@
shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
by (rewrite at asm assms)
+(* Rewriting "at asm" selects each full assumption, not any parts *)
+lemma
+ assumes "(PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP S \<Longrightarrow> PROP R)"
+ shows "PROP S \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP R"
+ apply (rewrite at asm assms)
+ apply assumption
+ done
+
(* Rewriting with conditional rewriting rules works just as well. *)