1.1 --- a/src/Pure/Proof/proofchecker.ML	Wed Dec 31 19:54:03 2008 +0100
     1.2 +++ b/src/Pure/Proof/proofchecker.ML	Wed Dec 31 19:54:04 2008 +0100
     1.3 @@ -30,8 +30,7 @@
     1.4  
     1.5  fun thm_of_proof thy prf =
     1.6    let
     1.7 -    val prf_names = Proofterm.fold_proof_terms
     1.8 -      (fold_aterms (fn Free (x, _) => Name.declare x | _ => I)) (K I) prf Name.context;
     1.9 +    val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
    1.10      val lookup = lookup_thm thy;
    1.11  
    1.12      fun thm_of_atom thm Ts =

     2.1 --- a/src/Tools/code/code_thingol.ML	Wed Dec 31 19:54:03 2008 +0100
     2.2 +++ b/src/Tools/code/code_thingol.ML	Wed Dec 31 19:54:04 2008 +0100
     2.3 @@ -707,8 +707,7 @@
     2.4          let
     2.5            val k = length ts;
     2.6            val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
     2.7 -          val ctxt = (fold o fold_aterms)
     2.8 -            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
     2.9 +          val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
    2.10            val vs = Name.names ctxt "a" tys;
    2.11          in
    2.12            fold_map (translate_typ thy algbr funcgr) tys