diff -r 0b08f218f260 -r 290454649b8c src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Apr 15 14:31:44 2007 +0200
+++ b/src/Pure/variable.ML	Sun Apr 15 14:31:47 2007 +0200
@@ -206,7 +206,7 @@
 
 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
 
-val declare_thm = Drule.fold_terms declare_internal;
+val declare_thm = Thm.fold_terms declare_internal;
 fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
 
 
@@ -444,7 +444,7 @@
 
 fun focus_subgoal i st =
   let
-    val all_vars = Drule.fold_terms Term.add_vars st [];
+    val all_vars = Thm.fold_terms Term.add_vars st [];
     val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
   in
     add_binds no_binds #>