src/FOLP/simp.ML
changeset 35021 c839a4c670c6
parent 33955 fff6f11b1f09
child 36603 d5d6111761a6
     1.1 --- a/src/FOLP/simp.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/FOLP/simp.ML	Sun Feb 07 19:33:34 2010 +0100
     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 Drule.standard subst_thms;
     1.8 +val subst_thms = map Drule.export_without_context subst_thms;
     1.9  
    1.10  
    1.11  fun exp_app(0,t) = t