# HG changeset patch
# User wenzelm
# Date 951660824 -3600
# Node ID 52d9f64841d6d13c03da8b55334a951d81f7e971
# Parent  9b089bc07f69cc6457e3496556fa83f22d526e92
added major_prem_of;

diff -r 9b089bc07f69 -r 52d9f64841d6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Feb 27 15:07:53 2000 +0100
+++ b/src/Pure/thm.ML	Sun Feb 27 15:13:44 2000 +0100
@@ -180,6 +180,7 @@
 signature THM =
 sig
   include BASIC_THM
+  val major_prem_of	: thm -> term
   val no_prems		: thm -> bool
   val no_attributes	: 'a -> 'a * 'b attribute list
   val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
@@ -477,6 +478,11 @@
 fun nprems_of (Thm {prop, ...}) =
   Logic.count_prems (Logic.skip_flexpairs prop, 0);
 
+fun major_prem_of thm =
+  (case prems_of thm of
+    prem :: _ => prem
+  | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm]));
+
 fun no_prems thm = nprems_of thm = 0;
 
 (*maps object-rule to conclusion*)