src/Pure/proofterm.ML
changeset 70540 04ef5ee3dd4d
parent 70538 fc9ba6fe367f
child 70541 f3fbc7f3559d
     1.1 --- a/src/Pure/proofterm.ML	Thu Aug 15 18:21:12 2019 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu Aug 15 19:35:17 2019 +0200
     1.3 @@ -168,9 +168,6 @@
     1.4    val standard_vars: Name.context -> term list * proof list -> term list * proof list
     1.5    val standard_vars_term: Name.context -> term -> term
     1.6    val standard_vars_proof: Name.context -> proof -> proof
     1.7 -  val used_frees_type: typ -> Name.context -> Name.context
     1.8 -  val used_frees_term: term -> Name.context -> Name.context
     1.9 -  val used_frees_proof: proof -> Name.context -> Name.context
    1.10  
    1.11    val proof_serial: unit -> proof_serial
    1.12    val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
    1.13 @@ -2046,25 +2043,25 @@
    1.14    | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
    1.15    | variant_proof _ prf = prf;
    1.16  
    1.17 +val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
    1.18 +fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
    1.19 +val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
    1.20 +
    1.21 +val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
    1.22 +val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
    1.23 +
    1.24  in
    1.25  
    1.26  fun standard_vars used (terms, proofs) =
    1.27    let
    1.28 +    val used' = used
    1.29 +      |> fold used_frees_term terms
    1.30 +      |> fold used_frees_proof proofs;
    1.31      val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
    1.32 -    val inst = Term_Subst.zero_var_indexes_inst used (terms @ proof_terms);
    1.33 -
    1.34 -    val is_used = Name.is_declared used o Name.clean;
    1.35 -    fun unvarifyT ty = ty |> Term.map_atyps
    1.36 -      (fn TVar ((a, _), S) => TFree (a, S)
    1.37 -        | T as TFree (a, _) => if is_used a then T else raise TYPE (Logic.bad_fixed a, [ty], [])
    1.38 -        | T => T);
    1.39 -    fun unvarify tm = tm |> Term.map_aterms
    1.40 -      (fn Var ((x, _), T) => Free (x, T)
    1.41 -        | t as Free (x, _) => if is_used x then t else raise TERM (Logic.bad_fixed x, [tm])
    1.42 -        | t => t);
    1.43 +    val inst = Term_Subst.zero_var_indexes_inst used' (terms @ proof_terms);
    1.44  
    1.45      val terms' = terms
    1.46 -      |> map (Term_Subst.instantiate inst #> unvarify #> map_types unvarifyT #> variant_term []);
    1.47 +      |> map (Term_Subst.instantiate inst #> unvarify #> variant_term []);
    1.48      val proofs' = proofs
    1.49        |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
    1.50    in (terms', proofs') end;
    1.51 @@ -2074,10 +2071,6 @@
    1.52  
    1.53  end;
    1.54  
    1.55 -val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
    1.56 -fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
    1.57 -val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
    1.58 -
    1.59  
    1.60  (* PThm nodes *)
    1.61  
    1.62 @@ -2109,10 +2102,7 @@
    1.63  
    1.64  fun export_proof thy i prop prf =
    1.65    let
    1.66 -    val free_names = Name.context
    1.67 -      |> used_frees_term prop
    1.68 -      |> used_frees_proof prf;
    1.69 -    val ([prop'], [prf']) = standard_vars free_names ([prop], [reconstruct_proof thy prop prf]);
    1.70 +    val ([prop'], [prf']) = standard_vars Name.context ([prop], [reconstruct_proof thy prop prf]);
    1.71      val xml = encode_export prop' prf';
    1.72      val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
    1.73    in