added comment
authorpaulson
Tue May 17 17:01:35 2005 +0200 (2005-05-17)
changeset 15977aa6744dd998e
parent 15976 44f615d1729b
child 15978 f044579b147c
added comment
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Tue May 17 17:01:19 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue May 17 17:01:35 2005 +0200
     1.3 @@ -215,7 +215,12 @@
     1.4          val assumed = implies_elim_list frozth (map assume froz_prems)
     1.5          val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
     1.6                                          assumed;
     1.7 -    in  Seq.single (thawfn implied)  end
     1.8 +    in  (*Applying Thm.varifyT to the result of thawfn would (re-)generalize
     1.9 +          all type variables that appear in the subgoals. Unfortunately, it
    1.10 +          would also break the function AxClass.intro_classes_tac, even in the
    1.11 +          trivial case where the type class has no axioms.*)
    1.12 +        Seq.single (thawfn implied)
    1.13 +    end
    1.14  end;
    1.15  
    1.16