Tried to reorganize rewriter a little. More to be done.

--- a/src/Pure/logic.ML	Fri Feb 27 11:21:28 1998 +0100
+++ b/src/Pure/logic.ML	Sat Feb 28 15:40:03 1998 +0100
@@ -324,11 +324,11 @@
   orelse
    (null prems andalso
     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
-  orelse
+(*  orelse
    (case lhs of
       (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
                                  (null prems andalso f occs rhs)
-    | _ => false);
+    | _ => false)*);
 (*the condition "null prems" in the last cases is necessary because
   conditional rewrites with extra variables in the conditions may terminate
   although the rhs is an instance of the lhs. Example:

--- a/src/Pure/pattern.ML	Fri Feb 27 11:21:28 1998 +0100
+++ b/src/Pure/pattern.ML	Sat Feb 28 15:40:03 1998 +0100
@@ -25,6 +25,7 @@
   val match             : type_sig -> term * term
                           -> (indexname*typ)list * (indexname*term)list
   val matches           : type_sig -> term * term -> bool
+  val matches_subterm   : type_sig -> term * term -> bool
   val unify             : sg * env * (term * term)list -> env
   exception Unif
   exception MATCH
@@ -390,4 +391,15 @@
 (*Predicate: does the pattern match the object?*)
 fun matches tsig po = (match tsig po; true) handle MATCH => false;
 
+(* Does pat match a subterm of obj? *)
+fun matches_subterm tsig (pat,obj) =
+  let fun msub(bounds,obj) = matches tsig (pat,obj) orelse
+            case obj of
+              Abs(x,T,t) => let val y = variant bounds x
+                                val f = Free(":" ^ y,T)
+                            in msub(x::bounds,subst_bound(f,t)) end
+            | s$t => msub(bounds,s) orelse msub(bounds,t)
+            | _ => false
+  in msub([],obj) end;
+
 end;

--- a/src/Pure/thm.ML	Fri Feb 27 11:21:28 1998 +0100
+++ b/src/Pure/thm.ML	Sat Feb 28 15:40:03 1998 +0100
@@ -164,7 +164,7 @@
   val add_prems         : meta_simpset * thm list -> meta_simpset
   val prems_of_mss      : meta_simpset -> thm list
   val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
-  val mk_rews_of_mss    : meta_simpset -> thm -> thm list
+(*  val mk_rews_of_mss    : meta_simpset -> thm -> thm list *)
   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
   val trace_simp        : bool ref
   val rewrite_cterm     : bool * bool -> meta_simpset ->
@@ -1575,33 +1575,39 @@
 
 (* add_simps *)
 
-fun add_simp
-  (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
-    thm as Thm {sign_ref, prop, ...}) =
-  (case mk_rrule thm of
+fun add_simp1(mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
+              thm as Thm {sign_ref, prop, ...}) =
+  case mk_rrule thm of
     None => mss
   | Some (rrule as {lhs, ...}) =>
       (trace_thm false "Adding rewrite rule:" thm;
-        mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule) handle Net.INSERT =>
-          (prtm true "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop; rules),
-            congs, procs, bounds, prems, mk_rews, termless)));
+       mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule),
+               congs, procs, bounds, prems, mk_rews, termless)
+       handle Net.INSERT =>
+       (prtm true "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop;
+        mss));
+
+fun add_simp(mss as Mss{mk_rews,...},thm) = foldl add_simp1 (mss, mk_rews thm);
 
 val add_simps = foldl add_simp;
 
-fun mss_of thms = add_simps (empty_mss, thms);
+fun mss_of thms = foldl add_simp1 (empty_mss, thms);
 
 
 (* del_simps *)
 
-fun del_simp
-  (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
-    thm as Thm {sign_ref, prop, ...}) =
-  (case mk_rrule thm of
+fun del_simp1(mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
+              thm as Thm {sign_ref, prop, ...}) =
+  case mk_rrule thm of
     None => mss
   | Some (rrule as {lhs, ...}) =>
-      mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule) handle Net.DELETE =>
-        (prtm true "rewrite rule not in simpset" (Sign.deref sign_ref) prop; rules),
-          congs, procs, bounds, prems, mk_rews, termless));
+      (mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule),
+               congs, procs, bounds, prems, mk_rews, termless)
+       handle Net.DELETE =>
+       (prtm true "rewrite rule not in simpset" (Sign.deref sign_ref) prop;
+        mss));
+
+fun del_simp(mss as Mss{mk_rews,...},thm) = foldl del_simp1 (mss, mk_rews thm);
 
 val del_simps = foldl del_simp;
 
@@ -1951,7 +1957,7 @@
                end)
          | _ => None)
 
-     and impc(shyps, hyps, s, u, mss as Mss{mk_rews,...}, ders) =
+     and impc(shyps, hyps, s, u, mss, ders) =
        let val (shyps1,hyps1,s1,ders1) =
              if simprem then try_botc mss (shyps,hyps,s,ders)
                         else (shyps,hyps,s,ders);
@@ -1963,7 +1969,7 @@
                                                   (Sign.deref sign_ref) s1; mss)
              else let val thm = assume (Cterm{sign_ref=sign_ref, t=s1, 
                                               T=propT, maxidx= ~1})
-                  in add_simps(add_prems(mss,[thm]), mk_rews thm) end
+                  in add_simp(add_prems(mss,[thm]), thm) end
            val (shyps2,hyps2,u1,ders2) = try_botc mss1 (shyps1,hyps1,u,ders1)
            val hyps3 = if gen_mem (op aconv) (s1, hyps1)
                        then hyps2 else hyps2\s1