src/HOL/Tools/choice_specification.ML
changeset 36945 9bec62c10714
parent 36618 7a0990473e03
child 36954 ef698bd61057
     1.1 --- a/src/HOL/Tools/choice_specification.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4                  fun process_single ((name,atts),rew_imp,frees) args =
     1.5                      let
     1.6                          fun undo_imps thm =
     1.7 -                            equal_elim (symmetric rew_imp) thm
     1.8 +                            Thm.equal_elim (Thm.symmetric rew_imp) thm
     1.9  
    1.10                          fun add_final (arg as (thy, thm)) =
    1.11                              if name = ""