# HG changeset patch
# User wenzelm
# Date 1150234912 -7200
# Node ID 47937afefdc9fe2e85d73218d89e2dc5c4c56d50
# Parent  1b0d48257caf1dd4cbf2f4d8817533958974392d
added hyps_of;
tuned;

diff -r 1b0d48257caf -r 47937afefdc9 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jun 13 23:41:49 2006 +0200
+++ b/src/Pure/thm.ML	Tue Jun 13 23:41:52 2006 +0200
@@ -75,7 +75,6 @@
   val eq_thms: thm list * thm list -> bool
   val theory_of_thm: thm -> theory
   val sign_of_thm: thm -> theory    (*obsolete*)
-  val maxidx_of: thm -> int
   val prop_of: thm -> term
   val proof_of: thm -> Proofterm.proof
   val tpairs_of: thm -> (term * term) list
@@ -116,7 +115,6 @@
   val unconstrainT: ctyp -> thm -> thm
   val varifyT: thm -> thm
   val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
-  val freezeT: thm -> thm
   val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
@@ -149,6 +147,8 @@
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
   val terms_of_tpairs: (term * term) list -> term list
+  val maxidx_of: thm -> int
+  val hyps_of: thm -> term list
   val full_prop_of: thm -> term
   val get_name_tags: thm -> string * tag list
   val put_name_tags: string * tag list -> thm -> thm
@@ -161,6 +161,7 @@
   val cterm_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   val cterm_first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   val cterm_incr_indexes: int -> cterm -> cterm
+  val freezeT: thm -> thm
 end;
 
 structure Thm: THM =
@@ -446,6 +447,7 @@
 val sign_of_thm = theory_of_thm;
 
 fun maxidx_of (Thm {maxidx, ...}) = maxidx;
+fun hyps_of (Thm {hyps, ...}) = hyps;
 fun prop_of (Thm {prop, ...}) = prop;
 fun proof_of (Thm {der = (_, proof), ...}) = proof;
 fun tpairs_of (Thm {tpairs, ...}) = tpairs;