changeset 11692 | 6d15ae4b1123 |
parent 11612 | ae8450657bf0 |
child 12500 | 0a6667d65e9b |
--- a/src/Pure/thm.ML Thu Oct 04 16:09:12 2001 +0200 +++ b/src/Pure/thm.ML Thu Oct 04 23:27:01 2001 +0200 @@ -358,7 +358,7 @@ fun major_prem_of thm = (case prems_of thm of - prem :: _ => prem + prem :: _ => Logic.strip_assums_concl prem | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm])); fun no_prems thm = nprems_of thm = 0;