author | paulson |

Tue May 17 17:01:35 2005 +0200 (2005-05-17) | |

changeset 15977 | aa6744dd998e |

parent 15976 | 44f615d1729b |

child 15978 | f044579b147c |

added comment

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