src/Tools/eqsubst.ML
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 *)