# HG changeset patch
# User wenzelm
# Date 1268489576 -3600
# Node ID 9c97d4e2450ef6c81ccc800966df46566555b835
# Parent  1416f568b2b62b86fe73b662d11aa670c44e5ee7
more antiquotations;

diff -r 1416f568b2b6 -r 9c97d4e2450e src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Mar 13 15:12:47 2010 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Mar 13 15:12:56 2010 +0100
@@ -614,7 +614,7 @@
       (let
         (* Term.term -> Term.typ option *)
         fun type_of_type_definition (Const (s', T')) =
-          if s'="Typedef.type_definition" then
+          if s'= @{const_name type_definition} then
             SOME T'
           else
             NONE