# HG changeset patch
# User wenzelm
# Date 1272896807 -7200
# Node ID b6c031ad3690adaf04ddf7b781dec53efbed5e95
# Parent  f3157c288aca7e8505789b3fb90707220ba44597
minor tuning of Thm.strip_shyps -- no longer pervasive;

diff -r f3157c288aca -r b6c031ad3690 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Mon May 03 16:26:47 2010 +0200
@@ -2065,7 +2065,7 @@
     let
         val (HOLThm args) = norm_hthm (theory_of_thm th) hth
     in
-        apsnd strip_shyps args
+        apsnd Thm.strip_shyps args
     end
 
 fun to_isa_term tm = tm
diff -r f3157c288aca -r b6c031ad3690 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon May 03 16:26:47 2010 +0200
@@ -502,7 +502,7 @@
             t |> disamb_bound thy
               |> chain (Simplifier.full_rewrite ss)
               |> chain eta_conversion
-              |> strip_shyps
+              |> Thm.strip_shyps
         val _ = message ("norm_term: " ^ (string_of_thm th))
     in
         th
diff -r f3157c288aca -r b6c031ad3690 src/HOL/Matrix/cplex/matrixlp.ML
--- a/src/HOL/Matrix/cplex/matrixlp.ML	Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML	Mon May 03 16:26:47 2010 +0200
@@ -81,7 +81,7 @@
 fun matrix_simplify th =
     let
         val simp_th = matrix_compute (cprop_of th)
-        val th = strip_shyps (equal_elim simp_th th)
+        val th = Thm.strip_shyps (equal_elim simp_th th)
         fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
     in
         removeTrue th
diff -r f3157c288aca -r b6c031ad3690 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Mon May 03 16:26:47 2010 +0200
@@ -436,8 +436,8 @@
 					val var  = new_free ()
 					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
 					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
-					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
-					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
+					val thm4 = Thm.strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
+					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
 				in
 					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
 				end
@@ -447,8 +447,8 @@
 					val var  = new_free ()
 					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
 					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
-					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
-					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
+					val thm4 = Thm.strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
+					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
 				in
 					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
 				end
@@ -467,8 +467,8 @@
 			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
 			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
 			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
-			val thm4 = strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
-			val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
+			val thm4 = Thm.strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
+			val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
 		in
 			iff_trans OF [thm1, thm5]
 		end
diff -r f3157c288aca -r b6c031ad3690 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon May 03 15:34:55 2010 +0200
+++ b/src/Pure/thm.ML	Mon May 03 16:26:47 2010 +0200
@@ -69,7 +69,6 @@
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
-  val strip_shyps: thm -> thm
 
   (*meta rules*)
   val assume: cterm -> thm
@@ -138,6 +137,7 @@
   val varifyT_global: thm -> thm
   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 freezeT: thm -> thm
@@ -476,26 +476,6 @@
     val sorts' = Sorts.union sorts more_sorts;
   in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
 
-
-
-(** sort contexts of theorems **)
-
-(*remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
-  | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
-      let
-        val thy = Theory.deref thy_ref;
-        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
-        val extra = fold (Sorts.remove_sort o #2) present shyps;
-        val witnessed = Sign.witness_sorts thy present extra;
-        val extra' = fold (Sorts.remove_sort o #2) witnessed extra
-          |> Sorts.minimal_sorts (Sign.classes_of thy);
-        val shyps' = fold (Sorts.insert_sort o #2) present extra';
-      in
-        Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
-          shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
-      end;
-
 (*dangling sort constraints of a thm*)
 fun extra_shyps (th as Thm (_, {shyps, ...})) =
   Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
@@ -1219,6 +1199,22 @@
     else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
   end;
 
+(*Remove extra sorts that are witnessed by type signature information*)
+fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
+  | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
+      let
+        val thy = Theory.deref thy_ref;
+        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
+        val extra = fold (Sorts.remove_sort o #2) present shyps;
+        val witnessed = Sign.witness_sorts thy present extra;
+        val extra' = fold (Sorts.remove_sort o #2) witnessed extra
+          |> Sorts.minimal_sorts (Sign.classes_of thy);
+        val shyps' = fold (Sorts.insert_sort o #2) present extra';
+      in
+        Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
+          shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
+      end;
+
 (*Internalize sort constraints of type variable*)
 fun unconstrainT
     (Ctyp {thy_ref = thy_ref1, T, ...})