# 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