# HG changeset patch
# User wenzelm
# Date 1146345406 -7200
# Node ID 56541f86094afbf53cbefba13fd67fdb8358b211
# Parent  10921826b160dbe77a4cb77e6b48cf617a9a3527
added unconstrainTs;

diff -r 10921826b160 -r 56541f86094a src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Apr 29 23:16:45 2006 +0200
+++ b/src/Pure/drule.ML	Sat Apr 29 23:16:46 2006 +0200
@@ -128,6 +128,7 @@
   val vars_of: thm -> (indexname * typ) list
   val tfrees_of: thm -> (string * sort) list
   val frees_of: thm -> (string * typ) list
+  val unconstrainTs: thm -> thm
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
   val rename_bvars: (string * string) list -> thm -> thm
   val rename_bvars': string option list -> thm -> thm
@@ -320,6 +321,9 @@
 fun tfrees_of th = rev (fold_terms Term.add_tfrees th []);
 fun frees_of th = rev (fold_terms Term.add_frees th []);
 
+fun unconstrainTs th =
+  fold_rev (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar) (tvars_of th) th;
+
 (*Strip extraneous shyps as far as possible*)
 fun strip_shyps_warning thm =
   let