tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
right sides of the defs

--- a/src/Pure/tactic.ML	Fri Oct 22 10:31:19 1993 +0100
+++ b/src/Pure/tactic.ML	Fri Oct 22 11:25:15 1993 +0100
@@ -376,20 +376,41 @@
 fun asm_rewrite_goal_tac prover_tac mss i =
       PRIMITIVE(rewrite_goal_rule (result1 prover_tac) mss i);
 
-(*Rewrite or fold throughout proof state. *)
-fun rewrite_tac thms = PRIMITIVE(rewrite_rule thms);
-fun fold_tac rths = rewrite_tac (map symmetric rths);
+(*Rewrite throughout proof state. *)
+fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
 
 (*Rewrite subgoals only, not main goal. *)
-fun rewrite_goals_tac thms = PRIMITIVE (rewrite_goals_rule thms);
-fun fold_goals_tac rths = rewrite_goals_tac (map symmetric rths);
+fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 
-fun rewtac rth = rewrite_goals_tac [rth];
+fun rewtac def = rewrite_goals_tac [def];
 
 
-(** Renaming of parameters in a subgoal
-    Names may contain letters, digits or primes and must be
-    separated by blanks **)
+(*** Tactic for folding definitions, handling critical pairs ***)
+
+(*The depth of nesting in a term*)
+fun term_depth (Abs(a,T,t)) = 1 + term_depth t
+  | term_depth (f$t) = 1 + max [term_depth f, term_depth t]
+  | term_depth _ = 0;
+
+val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;
+
+(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
+  Returns longest lhs first to avoid folding its subexpressions.*)
+fun sort_lhs_depths defs =
+  let val keylist = make_keylist (term_depth o lhs_of_thm) defs
+      val keys = distinct (sort op> (map #2 keylist))
+  in  map (keyfilter keylist) keys  end;
+
+fun fold_tac defs = EVERY 
+    (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
+
+fun fold_goals_tac defs = EVERY 
+    (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
+
+
+(*** Renaming of parameters in a subgoal
+     Names may contain letters, digits or primes and must be
+     separated by blanks ***)
 
 (*Calling this will generate the warning "Same as previous level" since
   it affects nothing but the names of bound variables!*)