# HG changeset patch
# User wenzelm
# Date 1273425321 -7200
# Node ID 46be8612797250c9616c5e73d558e328f0946852
# Parent  d0095729e1f15bf9b834418ecdf20e54234db423
just one version of Thm.unconstrainT, which affects all variables;
temporary workaround for Nbe.lift_triv_classes_conv;

diff -r d0095729e1f1 -r 46be86127972 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun May 09 18:09:30 2010 +0200
+++ b/src/HOL/HOL.thy	Sun May 09 19:15:21 2010 +0200
@@ -1869,7 +1869,7 @@
 proof
   assume "PROP ?ofclass"
   show "PROP ?eq"
-    by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *}) 
+    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *})
       (fact `PROP ?ofclass`)
 next
   assume "PROP ?eq"
diff -r d0095729e1f1 -r 46be86127972 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun May 09 18:09:30 2010 +0200
+++ b/src/Pure/axclass.ML	Sun May 09 19:15:21 2010 +0200
@@ -423,7 +423,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])))] []
-      |> Thm.unconstrain_allTs;
+      |> Thm.unconstrainT;
     val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
   in
     thy
@@ -449,7 +449,7 @@
       |> (map o apsnd o map_atyps) (K T);
     val th' = th
       |> Drule.instantiate' std_vars []
-      |> Thm.unconstrain_allTs;
+      |> Thm.unconstrainT;
     val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
   in
     thy
diff -r d0095729e1f1 -r 46be86127972 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun May 09 18:09:30 2010 +0200
+++ b/src/Pure/logic.ML	Sun May 09 19:15:21 2010 +0200
@@ -46,7 +46,7 @@
   val name_arity: string * sort list * class -> string
   val mk_arities: arity -> term list
   val dest_arity: term -> string * sort list * class
-  val unconstrain_allTs: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
+  val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
@@ -272,7 +272,7 @@
 
 (* internalized sort constraints *)
 
-fun unconstrain_allTs shyps prop =
+fun unconstrainT shyps prop =
   let
     val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
     val extra = fold (Sorts.remove_sort o #2) present shyps;
diff -r d0095729e1f1 -r 46be86127972 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun May 09 18:09:30 2010 +0200
+++ b/src/Pure/thm.ML	Sun May 09 19:15:21 2010 +0200
@@ -138,8 +138,7 @@
   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val of_class: ctyp * class -> thm
   val strip_shyps: thm -> thm
-  val unconstrainT: ctyp -> thm -> thm
-  val unconstrain_allTs: thm -> thm
+  val unconstrainT: thm -> thm
   val legacy_freezeT: thm -> thm
   val assumption: int -> thm -> thm Seq.seq
   val eq_assumption: int -> thm -> thm
@@ -1222,7 +1221,7 @@
       end;
 
 (*Internalize sort constraints of type variable*)
-fun unconstrainT
+fun unconstrain_TVar
     (Ctyp {thy_ref = thy_ref1, T, ...})
     (th as Thm (_, {thy_ref = thy_ref2, maxidx, shyps, hyps, tpairs, prop, ...})) =
   let
@@ -1242,8 +1241,8 @@
       prop = Logic.list_implies (constraints, unconstrain prop)})
   end;
 
-fun unconstrain_allTs th =
-  fold (unconstrainT o ctyp_of (theory_of_thm th) o TVar)
+fun unconstrainT th =
+  fold (unconstrain_TVar o ctyp_of (theory_of_thm th) o TVar)
     (fold_terms Term.add_tvars th []) th;
 
 
diff -r d0095729e1f1 -r 46be86127972 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sun May 09 18:09:30 2010 +0200
+++ b/src/Tools/nbe.ML	Sun May 09 19:15:21 2010 +0200
@@ -108,7 +108,9 @@
     |> Drule.cterm_rule Thm.legacy_freezeT
     |> conv
     |> Thm.varifyT_global
-    |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
+(* FIXME tmp *)
+(*    |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs*)
+    |> Thm.unconstrainT
     |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
         (((v, 0), []), TVar ((v, 0), sort))) vs, [])
     |> strip_of_class