--- a/src/HOL/Mutabelle/mutabelle.ML Tue Dec 07 16:27:07 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Tue Dec 07 17:23:14 2010 +0100
@@ -637,9 +637,9 @@
fun create_spaces entry spacenum =
let
- val diff = spacenum - (size entry)
- in
- if (diff > 0)
+ val diff = spacenum - (size entry)
+ in
+ if (diff > 0)
then implode (replicate diff " ")
else ""
end;
@@ -756,7 +756,7 @@
end;
(*exchange version of function mutqc_thystat*)
-
+
fun mutqc_thystat_exc p mutthy usedthy commutatives iter insts sz qciter filename =
mutqc_thystat 0 p mutthy usedthy commutatives [] iter insts sz qciter filename;