src/HOL/Tools/refute.ML
changeset 37117 59cee8807c29
parent 36692 54b64d4ad524
child 37254 3625d37a0079
     1.1 --- a/src/HOL/Tools/refute.ML	Tue May 25 20:22:55 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue May 25 20:28:16 2010 +0200
     1.3 @@ -588,7 +588,7 @@
     1.4          | NONE =>
     1.5            get_typedef_ax axioms
     1.6        end handle ERROR _         => get_typedef_ax axioms
     1.7 -               | MATCH           => get_typedef_ax axioms
     1.8 +               | TERM _          => get_typedef_ax axioms
     1.9                 | Type.TYPE_MATCH => get_typedef_ax axioms)
    1.10    in
    1.11      get_typedef_ax (Theory.all_axioms_of thy)