diff -r ddbbab501213 -r 197e00ce3f20 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Sep 09 11:10:16 2004 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Sep 10 00:19:15 2004 +0200
@@ -7,7 +7,7 @@
 
 infix 4
   addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
-  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
+  setmksimps setmksimps2 setmkcong setmksym setmkeqTrue settermless setsubgoaler
   setloop addloop delloop setSSolver addSSolver setSolver addSolver;
 
 signature BASIC_META_SIMPLIFIER =
@@ -30,6 +30,7 @@
     procs: proc Net.net,
     mk_rews:
      {mk: thm -> thm list,
+      mk2: thm list -> thm -> thm list,
       mk_cong: thm -> thm,
       mk_sym: thm -> thm option,
       mk_eq_True: thm -> thm option},
@@ -54,6 +55,7 @@
   val addsimprocs: simpset * simproc list -> simpset
   val delsimprocs: simpset * simproc list -> simpset
   val setmksimps: simpset * (thm -> thm list) -> simpset
+  val setmksimps2: simpset * (thm list -> thm -> thm list) -> simpset
   val setmkcong: simpset * (thm -> thm) -> simpset
   val setmksym: simpset * (thm -> thm option) -> simpset
   val setmkeqTrue: simpset * (thm -> thm option) -> simpset
@@ -203,6 +205,7 @@
       (functions that prove rewrite rules on the fly);
     mk_rews:
       mk: turn simplification thms into rewrite rules;
+      mk2: like mk but may also depend on the other premises
       mk_cong: prepare congruence rules;
       mk_sym: turn == around;
       mk_eq_True: turn P into P == True;
@@ -210,6 +213,7 @@
 
 type mk_rews =
  {mk: thm -> thm list,
+  mk2: thm list -> thm -> thm list,
   mk_cong: thm -> thm,
   mk_sym: thm -> thm option,
   mk_eq_True: thm -> thm option};
@@ -302,6 +306,7 @@
 
 val basic_mk_rews: mk_rews =
  {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
+  mk2 = fn thms => fn thm => [],
   mk_cong = I,
   mk_sym = Some o Drule.symmetric_fun,
   mk_eq_True = K None};
@@ -486,8 +491,11 @@
     else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   end;
 
-fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
-  flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
+fun extract_rews (Simpset ({prems, ...}, {mk_rews = {mk, ...}, ...}), thms)
+  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
+
+fun extract_rews2 (Simpset ({prems, ...}, {mk_rews = {mk2, ...}, ...}), thms)
+  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk2 prems thm)) thms);
 
 fun orient_comb_simps comb mk_rrule (ss, thms) =
   let
@@ -498,11 +506,20 @@
 fun extract_safe_rrules (ss, thm) =
   flat (map (orient_rrule ss) (extract_rews (ss, [thm])));
 
+fun extract_safe_rrules2 (ss, thm) =
+  flat (map (orient_rrule ss) (extract_rews2 (ss, [thm])));
+
 (*add rewrite rules explicitly; do not reorient!*)
 fun ss addsimps thms =
   orient_comb_simps (insert_rrule false) (mk_rrule ss) (ss, thms);
 
 
+fun add_prem2(ss,thm) =
+  foldl (insert_rrule true) (ss,extract_safe_rrules2(ss,thm))
+  |> add_prems [thm];
+
+fun add_prems2 thms ss = foldl add_prem2 (ss,thms);
+
 (* delsimps *)
 
 fun del_rrule (ss, rrule as {thm, elhs, ...}) =
@@ -617,26 +634,29 @@
 
 local
 
-fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True},
+fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk2, mk_cong, mk_sym, mk_eq_True},
       termless, subgoal_tac, loop_tacs, solvers) =>
-  let val (mk', mk_cong', mk_sym', mk_eq_True') = f (mk, mk_cong, mk_sym, mk_eq_True) in
-    (congs, procs, {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
+  let val (mk', mk2', mk_cong', mk_sym', mk_eq_True') = f (mk, mk2, mk_cong, mk_sym, mk_eq_True) in
+    (congs, procs, {mk = mk', mk2 = mk2', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
       termless, subgoal_tac, loop_tacs, solvers)
   end);
 
 in
 
-fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True) =>
-  (mk, mk_cong, mk_sym, mk_eq_True));
+fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk2, mk_cong, mk_sym, mk_eq_True) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
 
-fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True) =>
-  (mk, mk_cong, mk_sym, mk_eq_True));
+fun ss setmksimps2 mk2 = ss |> map_mk_rews (fn (mk, _, mk_cong, mk_sym, mk_eq_True) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
 
-fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True) =>
-  (mk, mk_cong, mk_sym, mk_eq_True));
+fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, mk2, _, mk_sym, mk_eq_True) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
 
-fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _) =>
-  (mk, mk_cong, mk_sym, mk_eq_True));
+fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk2, mk_cong, _, mk_eq_True) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
+
+fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk2, mk_cong, mk_sym, _) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
 
 end;
 
@@ -999,7 +1019,8 @@
         in (extract_safe_rrules (ss, asm), Some asm) end
 
     and add_rrules (rrss, asms) ss =
-      foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms)
+      let val Asms = mapfilter I asms
+      in foldl (insert_rrule true) (ss, flat rrss) |> add_prems2 Asms end
 
     and disch r (prem, eq) =
       let