summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 17 May 2005 17:01:35 +0200 | |

changeset 15977 | aa6744dd998e |

parent 15976 | 44f615d1729b |

child 15978 | f044579b147c |

added comment

--- 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;