# HG changeset patch
# User wenzelm
# Date 1332071504 -3600
# Node ID 6f00d8a83eb7285d51be3d364555d9f85fd1f4bb
# Parent  3094745a41efa0045ec8a43a8c36c8d439a47395
tuned;

diff -r 3094745a41ef -r 6f00d8a83eb7 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 18 10:28:31 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 18 12:51:44 2012 +0100
@@ -157,10 +157,9 @@
  | in_list_forb consSig (consNameStr,consType) ((forbNameStr,forbTypeStr)::xs) = 
    let 
      val forbType = Syntax.read_typ_global consSig forbTypeStr
-     val typeSignature = #tsig (Sign.rep_sg consSig)
    in
      if ((consNameStr = forbNameStr) 
-       andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT_global forbType))))
+       andalso (Sign.typ_instance consSig (consType,(Logic.varifyT_global forbType))))
      then true
      else in_list_forb consSig (consNameStr,consType) xs
    end;
@@ -173,12 +172,11 @@
 fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 
  let 
    val sigConsTypeList = consts_of consSig;
-   val typeSignature = #tsig (Sign.rep_sg consSig)
  in 
    let 
      fun recursiveSearch mutatableTermList [] = mutatableTermList
        | recursiveSearch mutatableTermList ((ConsName,ConsType)::xs) = 
-         if (Type.typ_instance typeSignature (stype,ConsType) 
+         if (Sign.typ_instance consSig (stype,ConsType) 
            andalso (not (sterm = Const(ConsName,stype))) 
            andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 
          then recursiveSearch ((Term.Const(ConsName,stype), [], [], [5])::mutatableTermList) xs