# HG changeset patch
# User wenzelm
# Date 1183475837 -7200
# Node ID 12271cfad085b9cd86e6a249018dfbd79196d654
# Parent  61ffcf4c02c73518b4ff0668d2de2526c28c7374
rewrite_goal_tac;

diff -r 61ffcf4c02c7 -r 12271cfad085 src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Tue Jul 03 17:17:16 2007 +0200
+++ b/src/ZF/UNITY/Constrains.thy	Tue Jul 03 17:17:17 2007 +0200
@@ -546,7 +546,7 @@
                                    constrains_imp_Constrains] 1),
               rtac constrainsI 1,
               (* Three subgoals *)
-              Goal.rewrite_goal_tac [st_set_def] 3,
+              rewrite_goal_tac [st_set_def] 3,
               REPEAT (Force_tac 2),
               full_simp_tac (ss addsimps !program_defs_ref) 1,
               ALLGOALS (clarify_tac cs),