thm_of_proof: improved generation of variables;
authorwenzelm
Wed Jul 19 12:12:07 2006 +0200 (2006-07-19)
changeset 20164928c8dc07216
parent 20163 08f2833ca433
child 20165 4de20306a88a
thm_of_proof: improved generation of variables;
src/Pure/Proof/proofchecker.ML
     1.1 --- a/src/Pure/Proof/proofchecker.ML	Wed Jul 19 12:12:06 2006 +0200
     1.2 +++ b/src/Pure/Proof/proofchecker.ML	Wed Jul 19 12:12:07 2006 +0200
     1.3 @@ -31,7 +31,8 @@
     1.4  
     1.5  fun thm_of_proof thy prf =
     1.6    let
     1.7 -    val names = Proofterm.fold_proof_terms Term.declare_term_names (K I) prf Name.context;
     1.8 +    val prf_names = Proofterm.fold_proof_terms
     1.9 +      (fold_aterms (fn Free (x, _) => Name.declare x | _ => I)) (K I) prf Name.context;
    1.10      val lookup = lookup_thm thy;
    1.11  
    1.12      fun thm_of_atom thm Ts =
    1.13 @@ -59,32 +60,32 @@
    1.14  
    1.15        | thm_of _ Hs (PBound i) = List.nth (Hs, i)
    1.16  
    1.17 -      | thm_of vs Hs (Abst (s, SOME T, prf)) =
    1.18 +      | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
    1.19            let
    1.20 -            val ([x], _) = Name.variants [s] (fold (Name.declare o fst) vs names);
    1.21 -            val thm = thm_of ((x, T) :: vs) Hs prf
    1.22 +            val ([x], names') = Name.variants [s] names;
    1.23 +            val thm = thm_of ((x, T) :: vs, names') Hs prf
    1.24            in
    1.25              Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
    1.26            end
    1.27  
    1.28 -      | thm_of vs Hs (prf % SOME t) =
    1.29 +      | thm_of (vs, names) Hs (prf % SOME t) =
    1.30            let
    1.31 -            val thm = thm_of vs Hs prf
    1.32 -            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t))
    1.33 +            val thm = thm_of (vs, names) Hs prf;
    1.34 +            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
    1.35            in Thm.forall_elim ct thm end
    1.36  
    1.37 -      | thm_of vs Hs (AbsP (s, SOME t, prf)) =
    1.38 +      | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
    1.39            let
    1.40              val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
    1.41 -            val thm = thm_of vs (Thm.assume ct :: Hs) prf
    1.42 +            val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
    1.43            in
    1.44              Thm.implies_intr ct thm
    1.45            end
    1.46  
    1.47 -      | thm_of vs Hs (prf %% prf') =
    1.48 +      | thm_of vars Hs (prf %% prf') =
    1.49            let
    1.50 -            val thm = beta_eta_convert (thm_of vs Hs prf);
    1.51 -            val thm' = beta_eta_convert (thm_of vs Hs prf')
    1.52 +            val thm = beta_eta_convert (thm_of vars Hs prf);
    1.53 +            val thm' = beta_eta_convert (thm_of vars Hs prf');
    1.54            in
    1.55              Thm.implies_elim thm thm'
    1.56            end
    1.57 @@ -93,6 +94,6 @@
    1.58  
    1.59        | thm_of _ _ _ = error "thm_of_proof: partial proof term";
    1.60  
    1.61 -  in beta_eta_convert (thm_of [] [] prf) end;
    1.62 +  in beta_eta_convert (thm_of ([], prf_names) [] prf) end;
    1.63  
    1.64  end;