thm_of_proof: tuned Name operations;
authorwenzelm
Tue Jul 18 20:01:47 2006 +0200 (2006-07-18)
changeset 20151b22c14181eb7
parent 20150 baa589c574ff
child 20152 b6373fe199e1
thm_of_proof: tuned Name operations;
src/Pure/Proof/proofchecker.ML
     1.1 --- a/src/Pure/Proof/proofchecker.ML	Tue Jul 18 20:01:46 2006 +0200
     1.2 +++ b/src/Pure/Proof/proofchecker.ML	Tue Jul 18 20:01:47 2006 +0200
     1.3 @@ -31,15 +31,14 @@
     1.4  
     1.5  fun thm_of_proof thy prf =
     1.6    let
     1.7 -    val names = add_prf_names ([], prf);
     1.8 -    val sg = sign_of thy;
     1.9 +    val names = Proofterm.fold_proof_terms Term.declare_term_names (K I) prf Name.context;
    1.10      val lookup = lookup_thm thy;
    1.11  
    1.12      fun thm_of_atom thm Ts =
    1.13        let
    1.14          val tvars = term_tvars (Thm.full_prop_of thm);
    1.15          val (fmap, thm') = Thm.varifyT' [] thm;
    1.16 -        val ctye = map (pairself (Thm.ctyp_of sg))
    1.17 +        val ctye = map (pairself (Thm.ctyp_of thy))
    1.18            (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
    1.19        in
    1.20          Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
    1.21 @@ -51,8 +50,8 @@
    1.22              val {prop, ...} = rep_thm thm;
    1.23              val _ = if prop aconv prop' then () else
    1.24                error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    1.25 -                Sign.string_of_term sg prop ^ "\n\n" ^
    1.26 -                Sign.string_of_term sg prop');
    1.27 +                Sign.string_of_term thy prop ^ "\n\n" ^
    1.28 +                Sign.string_of_term thy prop');
    1.29            in thm_of_atom thm Ts end
    1.30  
    1.31        | thm_of _ _ (PAxm (name, _, SOME Ts)) =
    1.32 @@ -62,35 +61,35 @@
    1.33  
    1.34        | thm_of vs Hs (Abst (s, SOME T, prf)) =
    1.35            let
    1.36 -            val x = Name.variant (names @ map fst vs) s;
    1.37 +            val ([x], _) = Name.variants [s] (fold (Name.declare o fst) vs names);
    1.38              val thm = thm_of ((x, T) :: vs) Hs prf
    1.39            in
    1.40 -            Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
    1.41 +            Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
    1.42            end
    1.43  
    1.44        | thm_of vs Hs (prf % SOME t) =
    1.45            let
    1.46              val thm = thm_of vs Hs prf
    1.47 -            val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t))
    1.48 +            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t))
    1.49            in Thm.forall_elim ct thm end
    1.50  
    1.51        | thm_of vs Hs (AbsP (s, SOME t, prf)) =
    1.52            let
    1.53 -            val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t));
    1.54 +            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
    1.55              val thm = thm_of vs (Thm.assume ct :: Hs) prf
    1.56            in
    1.57              Thm.implies_intr ct thm
    1.58            end
    1.59  
    1.60        | thm_of vs Hs (prf %% prf') =
    1.61 -          let 
    1.62 +          let
    1.63              val thm = beta_eta_convert (thm_of vs Hs prf);
    1.64              val thm' = beta_eta_convert (thm_of vs Hs prf')
    1.65            in
    1.66              Thm.implies_elim thm thm'
    1.67            end
    1.68  
    1.69 -      | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of sg t)
    1.70 +      | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
    1.71  
    1.72        | thm_of _ _ _ = error "thm_of_proof: partial proof term";
    1.73