src/Pure/thm.ML
changeset 28624 d983515e5cdf
parent 28446 a01de3b3fa2e
child 28648 4889b48919a0
     1.1 --- a/src/Pure/thm.ML	Thu Oct 16 22:44:32 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Oct 16 22:44:33 2008 +0200
     1.3 @@ -68,6 +68,7 @@
     1.4    val cprem_of: thm -> int -> cterm
     1.5    val transfer: theory -> thm -> thm
     1.6    val weaken: cterm -> thm -> thm
     1.7 +  val weaken_sorts: sort list -> cterm -> cterm
     1.8    val extra_shyps: thm -> sort list
     1.9    val strip_shyps: thm -> thm
    1.10    val get_axiom_i: theory -> string -> thm
    1.11 @@ -349,7 +350,7 @@
    1.12    hyps: term OrdList.T,                         (*hypotheses*)
    1.13    tpairs: (term * term) list,                   (*flex-flex pairs*)
    1.14    prop: term}                                   (*conclusion*)
    1.15 -and deriv = Deriv of                     
    1.16 +and deriv = Deriv of
    1.17   {oracle: bool,                                 (*oracle occurrence flag*)
    1.18    proof: Pt.proof,                              (*proof term*)
    1.19    promises: (serial * thm Future.T) OrdList.T}; (*promised derivations*)
    1.20 @@ -469,6 +470,14 @@
    1.21          prop = prop})
    1.22    end;
    1.23  
    1.24 +fun weaken_sorts raw_sorts ct =
    1.25 +  let
    1.26 +    val Cterm {thy_ref, t, T, maxidx, sorts} = ct;
    1.27 +    val thy = Theory.deref thy_ref;
    1.28 +    val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts);
    1.29 +    val sorts' = Sorts.union sorts more_sorts;
    1.30 +  in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
    1.31 +
    1.32  
    1.33  
    1.34  (** sort contexts of theorems **)
    1.35 @@ -484,7 +493,10 @@
    1.36          val thy = Theory.deref thy_ref;
    1.37          val present = present_sorts thm;
    1.38          val extra = Sorts.subtract present shyps;
    1.39 -        val shyps' = Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) shyps;
    1.40 +        val extra' =
    1.41 +          Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra
    1.42 +          |> Sorts.minimal_sorts (Sign.classes_of thy);
    1.43 +        val shyps' = Sorts.union present extra';
    1.44        in
    1.45          Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
    1.46            shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
    1.47 @@ -1644,7 +1656,7 @@
    1.48  
    1.49  fun future make_result ct =
    1.50    let
    1.51 -    val {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = rep_cterm ct;
    1.52 +    val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
    1.53      val thy = Context.reject_draft (Theory.deref thy_ref);
    1.54      val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
    1.55  
    1.56 @@ -1683,7 +1695,7 @@
    1.57  (* oracle rule *)
    1.58  
    1.59  fun invoke_oracle thy_ref1 name oracle arg =
    1.60 -  let val {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = rep_cterm (oracle arg) in
    1.61 +  let val Cterm {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = oracle arg in
    1.62      if T <> propT then
    1.63        raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
    1.64      else