added weaken_sorts;
strip_shyps: minimal list of minimized extra sorts;
tuned;

--- a/src/Pure/thm.ML	Thu Oct 16 22:44:32 2008 +0200
+++ b/src/Pure/thm.ML	Thu Oct 16 22:44:33 2008 +0200
@@ -68,6 +68,7 @@
   val cprem_of: thm -> int -> cterm
   val transfer: theory -> thm -> thm
   val weaken: cterm -> thm -> thm
+  val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
   val strip_shyps: thm -> thm
   val get_axiom_i: theory -> string -> thm
@@ -349,7 +350,7 @@
   hyps: term OrdList.T,                         (*hypotheses*)
   tpairs: (term * term) list,                   (*flex-flex pairs*)
   prop: term}                                   (*conclusion*)
-and deriv = Deriv of                     
+and deriv = Deriv of
  {oracle: bool,                                 (*oracle occurrence flag*)
   proof: Pt.proof,                              (*proof term*)
   promises: (serial * thm Future.T) OrdList.T}; (*promised derivations*)
@@ -469,6 +470,14 @@
         prop = prop})
   end;
 
+fun weaken_sorts raw_sorts ct =
+  let
+    val Cterm {thy_ref, t, T, maxidx, sorts} = ct;
+    val thy = Theory.deref thy_ref;
+    val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts);
+    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 **)
@@ -484,7 +493,10 @@
         val thy = Theory.deref thy_ref;
         val present = present_sorts thm;
         val extra = Sorts.subtract present shyps;
-        val shyps' = Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) shyps;
+        val extra' =
+          Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra
+          |> Sorts.minimal_sorts (Sign.classes_of thy);
+        val shyps' = Sorts.union present extra';
       in
         Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
@@ -1644,7 +1656,7 @@
 
 fun future make_result ct =
   let
-    val {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = rep_cterm ct;
+    val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
     val thy = Context.reject_draft (Theory.deref thy_ref);
     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
 
@@ -1683,7 +1695,7 @@
 (* oracle rule *)
 
 fun invoke_oracle thy_ref1 name oracle arg =
-  let val {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = rep_cterm (oracle arg) in
+  let val Cterm {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = oracle arg in
     if T <> propT then
       raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
     else