# HG changeset patch
# User wenzelm
# Date 938608807 -7200
# Node ID c3e5e85de4c3ceecb8219b878ae7efdc8d9210d9
# Parent  ae25e28e5ce941829a0fa6be835a273d4a50e042
removed force_strip_shyps;

diff -r ae25e28e5ce9 -r c3e5e85de4c3 src/HOL/AxClasses/Group/ROOT.ML
--- a/src/HOL/AxClasses/Group/ROOT.ML	Wed Sep 29 14:39:35 1999 +0200
+++ b/src/HOL/AxClasses/Group/ROOT.ML	Wed Sep 29 14:40:07 1999 +0200
@@ -8,18 +8,7 @@
 set show_types;
 set show_sorts;
 
-(*disable bug compatibility*)
-reset force_strip_shyps;
-
-set force_strip_shyps; (* FIXME tmp hack *)
-
-
-use_thy "Sigs";
-
 use_thy "Monoid";
 use_thy "Group";
-
 use_thy "MonoidGroupInsts";
-
-use_thy "GroupDefs";
 use_thy "GroupInsts";