Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Mutabelle/mutabelle.ML
changeset 36743 ce2297415b54
parent 36692 54b64d4ad524
child 37744 3daaf23b9ab4 
--- a/src/HOL/Mutabelle/mutabelle.ML	Sat May 08 16:24:44 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Sat May 08 17:10:27 2010 +0200
@@ -648,7 +648,7 @@
        val mutated = mutate option (prop_of x) usedthy
          commutatives forbidden_funs iter
        val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
-       val thmname =  "\ntheorem " ^ (Thm.get_name x) ^ ":"
+       val thmname =  "\ntheorem " ^ Thm.get_name_hint x ^ ":"
        val pnumstring = string_of_int passednum
        val cenumstring = string_of_int cenum
      in
isabelle