src/Pure/proofterm.ML
 changeset 36621 2fd4e2c76636 parent 36620 e6bb250402b5 child 36732 9c2ee10809b2
```     1.1 --- a/src/Pure/proofterm.ML	Tue May 04 12:30:15 2010 +0200
1.2 +++ b/src/Pure/proofterm.ML	Tue May 04 14:38:59 2010 +0200
1.3 @@ -108,6 +108,8 @@
1.4    val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
1.5    val equal_intr: term -> term -> proof -> proof -> proof
1.6    val equal_elim: term -> term -> proof -> proof -> proof
1.7 +  val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
1.8 +    sort list -> proof -> proof
1.9    val axm_proof: string -> term -> proof
1.10    val oracle_proof: string -> term -> oracle * proof
1.11    val promise_proof: theory -> serial -> term -> proof
1.12 @@ -884,6 +886,22 @@
1.13    equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
1.14
1.15
1.16 +(**** sort hypotheses ****)
1.17 +
1.18 +fun strip_shyps_proof algebra present witnessed extra_sorts prf =
1.19 +  let
1.20 +    fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
1.21 +    val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts;
1.22 +    val replacements = present @ extra @ witnessed;
1.23 +    fun replace T =
1.24 +      if exists (fn (T', _) => T' = T) present then raise Same.SAME
1.25 +      else
1.26 +        (case get_first (get (Type.sort_of_atyp T)) replacements of
1.27 +          SOME T' => T'
1.28 +        | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term");
1.29 +  in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
1.30 +
1.31 +
1.32  (***** axioms and theorems *****)
1.33
1.34  val proofs = Unsynchronized.ref 2;
```