removed obsolete Drule.frees/vars_of etc.;
authorwenzelm
Wed Aug 02 22:26:37 2006 +0200 (2006-08-02)
changeset 202864cf8e86a2d29
parent 20285 23f5cd23c1e1
child 20287 8cbcb46c3c09
removed obsolete Drule.frees/vars_of etc.;
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/datatype_realizer.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Aug 02 18:33:46 2006 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Aug 02 22:26:37 2006 +0200
     1.3 @@ -2199,8 +2199,10 @@
     1.4  		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
     1.5                      typedef_hol2hollight
     1.6  	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
     1.7 -            val _ = if Drule.tvars_of th4 = [] then () else raise ERR "type_introduction" "no type variables expected any more" 
     1.8 -            val _ = if Drule.vars_of th4 = [] then () else raise ERR "type_introduction" "no term variables expected any more"
     1.9 +            val _ = null (Drule.fold_terms Term.add_tvars th4 []) orelse
    1.10 +              raise ERR "type_introduction" "no type variables expected any more"
    1.11 +            val _ = null (Drule.fold_terms Term.add_vars th4 []) orelse
    1.12 +              raise ERR "type_introduction" "no term variables expected any more"
    1.13  	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
    1.14              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
    1.15  	    val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
     2.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Aug 02 18:33:46 2006 +0200
     2.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Aug 02 22:26:37 2006 +0200
     2.3 @@ -136,9 +136,8 @@
     2.4          ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
     2.5        ||> Theory.restore_naming thy;
     2.6  
     2.7 -    val ivs = Drule.vars_of_terms
     2.8 -      [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
     2.9 -    val rvs = Drule.vars_of_terms [prop_of thm'];
    2.10 +    val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
    2.11 +    val rvs = rev (Drule.fold_terms Term.add_vars thm' []);
    2.12      val ivs1 = map Var (filter_out (fn (_, T) =>
    2.13        tname_of (body_type T) mem ["set", "bool"]) ivs);
    2.14      val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
     3.1 --- a/src/Pure/codegen.ML	Wed Aug 02 18:33:46 2006 +0200
     3.2 +++ b/src/Pure/codegen.ML	Wed Aug 02 22:26:37 2006 +0200
     3.3 @@ -534,7 +534,7 @@
     3.4  fun rename_terms ts =
     3.5    let
     3.6      val names = foldr add_term_names
     3.7 -      (map (fst o fst) (Drule.vars_of_terms ts)) ts;
     3.8 +      (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
     3.9      val reserved = names inter ThmDatabase.ml_reserved;
    3.10      val (illegal, alt_names) = split_list (map_filter (fn s =>
    3.11        let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)