| changeset 60949 | ccbf9379e355 |
| parent 60818 | 5e11a6e2b044 |
| child 61075 | f6b0d827240e |
--- a/src/HOL/Tools/groebner.ML Sun Aug 16 18:19:30 2015 +0200 +++ b/src/HOL/Tools/groebner.ML Sun Aug 16 19:25:08 2015 +0200 @@ -496,7 +496,7 @@ fun simple_choose v th = choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v) - ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th + (Thm.dest_arg (hd (Thm.chyps_of th))))) th fun mkexi v th =