src/HOL/Tools/res_axioms.ML
changeset 22691 290454649b8c
parent 22644 f10465ee7aa2
child 22724 3002683a6e0f
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Apr 15 14:31:44 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Apr 15 14:31:47 2007 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4  
     1.5  (*Returns the vars of a theorem*)
     1.6  fun vars_of_thm th =
     1.7 -  map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
     1.8 +  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
     1.9  
    1.10  (*Make a version of fun_cong with a given variable name*)
    1.11  local