author | paulson |
Mon, 11 Mar 1996 14:16:35 +0100 | |
changeset 1566 | a203d206fab7 |
parent 1565 | 70dd38777109 |
child 1567 | 02bbdc811ae7 |
src/Pure/thm.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/thm.ML Mon Mar 11 14:13:36 1996 +0100 +++ b/src/Pure/thm.ML Mon Mar 11 14:16:35 1996 +0100 @@ -542,7 +542,7 @@ fun name_thm (thy, name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = if Sign.eq_sg (sign, sign_of thy) then Thm {sign = sign, - der = Infer (Theorem(thy,name), []), + der = Infer (Theorem(thy,name), [der]), maxidx = maxidx, shyps = shyps, hyps = hyps,