fixed axclass_tac;
authorwenzelm
Wed, 17 Mar 1999 16:53:32 +0100
changeset 6393 b8dafa978382
parent 6392 e2ecfd8622ae
child 6394 3d9fd50fcc43
fixed axclass_tac;
src/HOL/AxClasses/Tutorial/Xor.ML
--- a/src/HOL/AxClasses/Tutorial/Xor.ML	Wed Mar 17 16:45:53 1999 +0100
+++ b/src/HOL/AxClasses/Tutorial/Xor.ML	Wed Mar 17 16:53:32 1999 +0100
@@ -8,7 +8,7 @@
 open AxClass;
 
 goal_arity Xor.thy ("bool", [], "agroup");
-by (axclass_tac Xor.thy []);
+by (axclass_tac []);
 by (rewrite_goals_tac
       [Xor.prod_bool_def,Xor.inverse_bool_def, Xor.unit_bool_def]);
 by (ALLGOALS (Fast_tac));