# HG changeset patch
# User wenzelm
# Date 1272229772 -7200
# Node ID 0584e203960e36d9658fea6d37cd5342fd816921
# Parent  85004134055c9f06c7cf0bfecc224748dee9f2be
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
less pervasive names;

diff -r 85004134055c -r 0584e203960e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Apr 25 22:50:47 2010 +0200
+++ b/src/HOL/HOL.thy	Sun Apr 25 23:09:32 2010 +0200
@@ -1869,7 +1869,7 @@
 proof
   assume "PROP ?ofclass"
   show "PROP ?eq"
-    by (tactic {* ALLGOALS (rtac (Drule.unconstrainTs @{thm equals_eq})) *}) 
+    by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *}) 
       (fact `PROP ?ofclass`)
 next
   assume "PROP ?eq"
diff -r 85004134055c -r 0584e203960e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Apr 25 22:50:47 2010 +0200
+++ b/src/Pure/axclass.ML	Sun Apr 25 23:09:32 2010 +0200
@@ -431,7 +431,7 @@
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
     val th' = th
       |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] []
-      |> Drule.unconstrainTs;
+      |> Thm.unconstrain_allTs;
     val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
   in
     thy
@@ -455,7 +455,7 @@
     val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
     val th' = th
       |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names) []
-      |> Drule.unconstrainTs;
+      |> Thm.unconstrain_allTs;
     val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
   in
     thy
diff -r 85004134055c -r 0584e203960e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Apr 25 22:50:47 2010 +0200
+++ b/src/Pure/drule.ML	Sun Apr 25 23:09:32 2010 +0200
@@ -106,7 +106,6 @@
   val dummy_thm: thm
   val sort_constraintI: thm
   val sort_constraint_eq: thm
-  val unconstrainTs: thm -> thm
   val with_subgoal: int -> (thm -> thm) -> thm -> thm
   val comp_no_flatten: thm * int -> int -> thm -> thm
   val rename_bvars: (string * string) list -> thm -> thm
@@ -204,12 +203,6 @@
 
 (** Standardization of rules **)
 
-(* type classes and sorts *)
-
-fun unconstrainTs th =
-  fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar)
-    (Thm.fold_terms Term.add_tvars th []) th;
-
 (*Generalization over a list of variables*)
 val forall_intr_list = fold_rev forall_intr;
 
diff -r 85004134055c -r 0584e203960e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Apr 25 22:50:47 2010 +0200
+++ b/src/Pure/thm.ML	Sun Apr 25 23:09:32 2010 +0200
@@ -92,8 +92,6 @@
   val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
   val trivial: cterm -> thm
-  val of_class: ctyp * class -> thm
-  val unconstrainT: ctyp -> 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
@@ -139,6 +137,9 @@
   val adjust_maxidx_thm: int -> thm -> thm
   val varifyT_global: thm -> thm
   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+  val of_class: ctyp * class -> thm
+  val unconstrainT: ctyp -> thm -> thm
+  val unconstrain_allTs: thm -> thm
   val freezeT: thm -> thm
   val assumption: int -> thm -> thm Seq.seq
   val eq_assumption: int -> thm -> thm
@@ -1240,6 +1241,11 @@
       prop = Logic.list_implies (constraints, unconstrain prop)})
   end;
 
+fun unconstrain_allTs th =
+  fold (unconstrainT o ctyp_of (theory_of_thm th) o TVar)
+    (fold_terms Term.add_tvars th []) th;
+
+
 (* Replace all TFrees not fixed or in the hyps by new TVars *)
 fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   let