changeset 33259 | 17014b1b9353 |
parent 32962 | 69916a850301 |
child 36970 | 01594f816e3a |
1.1 --- a/src/Tools/eqsubst.ML Tue Oct 27 17:19:31 2009 +0100 1.2 +++ b/src/Tools/eqsubst.ML Tue Oct 27 17:34:00 2009 +0100 1.3 @@ -269,7 +269,7 @@ 1.4 (* FOR DEBUGGING... 1.5 type trace_subst_errT = int (* subgoal *) 1.6 * thm (* thm with all goals *) 1.7 - * (Thm.cterm list (* certified free var placeholders for vars *) 1.8 + * (cterm list (* certified free var placeholders for vars *) 1.9 * thm) (* trivial thm of goal concl *) 1.10 (* possible matches/unifiers *) 1.11 * thm (* rule *)