src/Pure/variable.ML
changeset 22691 290454649b8c
parent 22671 3c62305fbee6
child 22711 0b18739c3e81
     1.1 --- a/src/Pure/variable.ML	Sun Apr 15 14:31:44 2007 +0200
     1.2 +++ b/src/Pure/variable.ML	Sun Apr 15 14:31:47 2007 +0200
     1.3 @@ -206,7 +206,7 @@
     1.4  
     1.5  val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
     1.6  
     1.7 -val declare_thm = Drule.fold_terms declare_internal;
     1.8 +val declare_thm = Thm.fold_terms declare_internal;
     1.9  fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
    1.10  
    1.11  
    1.12 @@ -444,7 +444,7 @@
    1.13  
    1.14  fun focus_subgoal i st =
    1.15    let
    1.16 -    val all_vars = Drule.fold_terms Term.add_vars st [];
    1.17 +    val all_vars = Thm.fold_terms Term.add_vars st [];
    1.18      val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
    1.19    in
    1.20      add_binds no_binds #>