# HG changeset patch
# User paulson
# Date 959357203 -7200
# Node ID 8b7718296a35b390af54f1878bdcccaa15006166
# Parent  13ad7ce031bbec0b17f95560f6344c6e28a56024
tidied

diff -r 13ad7ce031bb -r 8b7718296a35 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Fri May 26 18:06:12 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Fri May 26 18:06:43 2000 +0200
@@ -531,7 +531,7 @@
 by (dtac act_subset_imp_project_act_subset 1);
 by (subgoal_tac
     "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1);
-by (rewrite_goals_tac [Restrict_def, project_set_def, extend_set_def, project_act_def]);
+by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]);
 (*using Int_greatest actually slows the next step!*)
 by (Blast_tac 2);
 by (force_tac (claset(),