1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -54,13 +54,13 @@
     1.4  
     1.5  (* beta contract the theorem *)
     1.6  fun beta_contract thm = 
     1.7 -    equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
     1.8 +    Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
     1.9  
    1.10  (* beta-eta contract the theorem *)
    1.11  fun beta_eta_contract thm = 
    1.12      let
    1.13 -      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    1.14 -      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    1.15 +      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    1.16 +      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    1.17      in thm3 end;
    1.18  
    1.19