# HG changeset patch
# User noschinl
# Date 1428931952 -7200
# Node ID 0e9895ffab1d3db8153b8542d306cd6cf8147a8e
# Parent  616a176402297bc30e7eaa8561e0bee095c90472
rewrite: do not descend into conclusion of premise with asm pattern

diff -r 616a17640229 -r 0e9895ffab1d src/HOL/Library/rewrite.ML
--- 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) =
diff -r 616a17640229 -r 0e9895ffab1d src/HOL/ex/Rewrite_Examples.thy
--- 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. *)