# HG changeset patch
# User paulson
# Date 1116342095 -7200
# Node ID aa6744dd998ec07df894e79901258f124d06a4ee
# Parent  44f615d1729bd9b0ebb593fb3aadd4a0b94d047a
added comment

diff -r 44f615d1729b -r aa6744dd998e src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue May 17 17:01:19 2005 +0200
+++ b/src/Pure/tactic.ML	Tue May 17 17:01:35 2005 +0200
@@ -215,7 +215,12 @@
         val assumed = implies_elim_list frozth (map assume froz_prems)
         val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
                                         assumed;
-    in  Seq.single (thawfn implied)  end
+    in  (*Applying Thm.varifyT to the result of thawfn would (re-)generalize
+          all type variables that appear in the subgoals. Unfortunately, it
+          would also break the function AxClass.intro_classes_tac, even in the
+          trivial case where the type class has no axioms.*)
+        Seq.single (thawfn implied)
+    end
 end;