src/Tools/coherent.ML
changeset 36945 9bec62c10714
parent 32740 9dd0a2f83429
child 36946 4eba866311df
     1.1 --- a/src/Tools/coherent.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/Tools/coherent.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -46,8 +46,8 @@
     1.4  fun rulify_elim_conv ct =
     1.5    if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
     1.6    else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
     1.7 -    (rewr_conv (symmetric Data.atomize_elimL) then_conv
     1.8 -     MetaSimplifier.rewrite true (map symmetric
     1.9 +    (rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
    1.10 +     MetaSimplifier.rewrite true (map Thm.symmetric
    1.11         [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
    1.12  
    1.13  end;