# HG changeset patch
# User wenzelm
# Date 1120250090 -7200
# Node ID 9a987b59ecab95790933010659a868ebe245c685
# Parent  b75568de32c60560161df24fd26bb565a896e001
cterm_aconv: avoid rep_cterm;

diff -r b75568de32c6 -r 9a987b59ecab src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Jul 01 22:33:59 2005 +0200
+++ b/src/Pure/tactic.ML	Fri Jul 01 22:34:50 2005 +0200
@@ -210,7 +210,7 @@
 
 (*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