src/FOLP/simp.ML
changeset 32957 675c0c7e6a37
parent 32952 aeb1e44fbc19
child 33040 cffdb7b28498
     1.1 --- a/src/FOLP/simp.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -519,7 +519,7 @@
     1.4  (* Compute Congruence rules for individual constants using the substition
     1.5     rules *)
     1.6  
     1.7 -val subst_thms = map standard subst_thms;
     1.8 +val subst_thms = map Drule.standard subst_thms;
     1.9  
    1.10  
    1.11  fun exp_app(0,t) = t