| changeset 12923 | 9ba7c5358fa0 |
| parent 12803 | 37131c76dff6 |
| child 12982 | 34a07757634d |
--- a/src/Pure/thm.ML Thu Feb 21 20:10:34 2002 +0100 +++ b/src/Pure/thm.ML Thu Feb 21 20:11:05 2002 +0100 @@ -494,7 +494,8 @@ (* name and tags -- make proof objects more readable *) -fun get_name_tags (Thm {prop, der = (_, prf), ...}) = Pt.get_name_tags prop prf; +fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) = + Pt.get_name_tags hyps prop prf; fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, shyps, hyps, prop}) = Thm {sign_ref = sign_ref,