src/Pure/Isar/proof.ML
changeset 8186 61ec7bedc717
parent 8166 97414b447a02
child 8206 e50a130ec9af
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Feb 02 13:26:38 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Feb 02 20:19:25 2000 +0100
     1.3 @@ -380,18 +380,11 @@
     1.4      |> Drule.forall_elim_vars 0
     1.5    end;
     1.6  
     1.7 -fun most_general_varify_tfrees thm =
     1.8 -  let
     1.9 -    val {hyps, prop, ...} = Thm.rep_thm thm;
    1.10 -    val frees = foldr Term.add_term_frees (prop :: hyps, []);
    1.11 -    val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
    1.12 -  in thm |> Thm.varifyT' leave_tfrees end;
    1.13 -
    1.14  fun export fixes casms thm =
    1.15    thm
    1.16    |> Drule.implies_intr_list casms
    1.17    |> varify_frees fixes
    1.18 -  |> most_general_varify_tfrees;
    1.19 +  |> ProofContext.most_general_varify_tfrees;
    1.20  
    1.21  fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner)
    1.22    | diff_context inner (Some outer) =
    1.23 @@ -476,7 +469,7 @@
    1.24        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
    1.25      else if not (t aconv prop) then
    1.26        err ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
    1.27 -    else Drule.forall_elim_vars (maxidx + 1) thm
    1.28 +    else thm |> Drule.forall_elim_vars (maxidx + 1) |> ProofContext.most_general_varify_tfrees
    1.29    end;
    1.30  
    1.31