src/Pure/tactic.ML

 val flexflex_tac = PRIMSEQ flexflex_rule;
 
 
 (*Remove duplicate subgoals.  By Mark Staples*)
 local
-fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b);
+fun cterm_aconv (a,b) = term_of a aconv term_of b;
 in
 fun distinct_subgoals_tac state =
     let val (frozth,thawfn) = freeze_thaw state
         val froz_prems = cprems_of frozth
         val assumed = implies_elim_list frozth (map assume froz_prems)