# HG changeset patch # User paulson # Date 912419139 -3600 # Node ID 4d00bbd3d3acd2f9372d45e94ff750e3fbb1234e # Parent 6b6e0ede35174ed6a3425c2e6afe82385131a361 tactical CHANGED now uses alpha-eta conversion, not alpha conversion Streamlined code diff -r 6b6e0ede3517 -r 4d00bbd3d3ac src/Pure/tctical.ML --- a/src/Pure/tctical.ML Mon Nov 30 10:44:05 1998 +0100 +++ b/src/Pure/tctical.ML Mon Nov 30 10:45:39 1998 +0100 @@ -327,12 +327,13 @@ (*Returns all states that have changed in subgoal i, counted from the LAST subgoal. For stac, for example.*) fun CHANGED_GOAL tac i st = - let val j = nprems_of st - i + let val j = nprems_of st val t = List.nth(prems_of st, i-1) - fun diff st' = - not (nprems_of st' > j (*subgoal is still there*) + fun diff st' = (*true if subgoal still exists and is same as old one*) + not (nprems_of st' >= j andalso - t aconv List.nth(prems_of st', nprems_of st' - j - 1)) + Pattern.aeconv (t, + List.nth(prems_of st', nprems_of st' - j))) in Seq.filter diff (tac i st) end handle Subscript => Seq.empty (*no subgoal i*);