# HG changeset patch
# User wenzelm
# Date 935606336 -7200
# Node ID 1e485129fbc189170a7bb58cf5a2d0fcb71721bb
# Parent  708bd83745c50f00c8f1ae7ad662cf9190bb50cd
expand_classes renamed to intro_classes;

diff -r 708bd83745c5 -r 1e485129fbc1 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Aug 25 18:53:49 1999 +0200
+++ b/src/Pure/axclass.ML	Wed Aug 25 20:38:56 1999 +0200
@@ -306,14 +306,14 @@
   end;
 
 
-(* expand classes *)
+(* intro_classes *)
 
-fun expand_classes_tac st =
+fun intro_classes_tac st =
   TRY (REPEAT_FIRST (resolve_tac (class_axms (Thm.sign_of_thm st)))) st;
 
-val expand_classes_method =
-  ("expand_classes", Method.no_args (Method.METHOD0 expand_classes_tac),
-    "expand axiomatic type classes");
+val intro_classes_method =
+  ("intro_classes", Method.no_args (Method.METHOD0 intro_classes_tac),
+    "back-chain introduction rules of axiomatic type classes");
 
 
 (* axclass_tac *)
@@ -328,7 +328,7 @@
     val defs = filter is_def thms;
     val non_defs = filter_out is_def thms;
   in
-    expand_classes_tac THEN
+    intro_classes_tac THEN
     TRY (rewrite_goals_tac defs) THEN
     TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
   end;
@@ -423,7 +423,7 @@
 
 val setup =
  [AxclassesData.init,
-  Method.add_methods [expand_classes_method]];
+  Method.add_methods [intro_classes_method]];
 
 
 (* outer syntax *)