1.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 18 10:28:31 2012 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 18 12:51:44 2012 +0100
     1.3 @@ -157,10 +157,9 @@
     1.4   | in_list_forb consSig (consNameStr,consType) ((forbNameStr,forbTypeStr)::xs) = 
     1.5     let 
     1.6       val forbType = Syntax.read_typ_global consSig forbTypeStr
     1.7 -     val typeSignature = #tsig (Sign.rep_sg consSig)
     1.8     in
     1.9       if ((consNameStr = forbNameStr) 
    1.10 -       andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT_global forbType))))
    1.11 +       andalso (Sign.typ_instance consSig (consType,(Logic.varifyT_global forbType))))
    1.12       then true
    1.13       else in_list_forb consSig (consNameStr,consType) xs
    1.14     end;
    1.15 @@ -173,12 +172,11 @@
    1.16  fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 
    1.17   let 
    1.18     val sigConsTypeList = consts_of consSig;
    1.19 -   val typeSignature = #tsig (Sign.rep_sg consSig)
    1.20   in 
    1.21     let 
    1.22       fun recursiveSearch mutatableTermList [] = mutatableTermList
    1.23         | recursiveSearch mutatableTermList ((ConsName,ConsType)::xs) = 
    1.24 -         if (Type.typ_instance typeSignature (stype,ConsType) 
    1.25 +         if (Sign.typ_instance consSig (stype,ConsType) 
    1.26             andalso (not (sterm = Const(ConsName,stype))) 
    1.27             andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 
    1.28           then recursiveSearch ((Term.Const(ConsName,stype), [], [], [5])::mutatableTermList) xs