src/HOL/Mutabelle/mutabelle.ML
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;