# HG changeset patch # User paulson # Date 826550195 -3600 # Node ID a203d206fab75236737a52b863afaae7725485cd # Parent 70dd38777109a5be38cda0ea3ebdda77d9298c42 name_thm: now keeps the previous deriviation! diff -r 70dd38777109 -r a203d206fab7 src/Pure/thm.ML --- 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,