changeset 35845 | e5980f0ad025 |
parent 35625 | 9c818cab0dd0 |
child 36610 | bafd82950e24 |
--- a/src/HOL/Mutabelle/mutabelle.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle.ML Sat Mar 20 17:33:11 2010 +0100 @@ -218,7 +218,7 @@ val typeSignature = #tsig (Sign.rep_sg consSig) in if ((consNameStr = forbNameStr) - andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT forbType)))) + andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT_global forbType)))) then true else in_list_forb consSig (consNameStr,consType) xs end;