src/Pure/tactic.ML
changeset 16666 9a987b59ecab
parent 16425 2427be27cc60
child 16809 8ca51a846576
     1.1 --- a/src/Pure/tactic.ML	Fri Jul 01 22:33:59 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Fri Jul 01 22:34:50 2005 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4  
     1.5  (*Remove duplicate subgoals.  By Mark Staples*)
     1.6  local
     1.7 -fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b);
     1.8 +fun cterm_aconv (a,b) = term_of a aconv term_of b;
     1.9  in
    1.10  fun distinct_subgoals_tac state =
    1.11      let val (frozth,thawfn) = freeze_thaw state