Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more antiquotations;
authorwenzelm
Sat, 13 Mar 2010 15:12:56 +0100
changeset 35746 9c97d4e2450e
parent 35745 1416f568b2b6
child 35760 22e6c38ebe25
more antiquotations;
src/HOL/Tools/refute.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle