--- a/src/HOL/Mutabelle/mutabelle.ML Tue Jul 20 22:03:37 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Tue Jul 20 23:09:49 2010 +0200
@@ -82,7 +82,7 @@
(*helper function in order to properly print a term*)
-fun prt x = Pretty.writeln (Syntax.pretty_term_global (theory "Main") x);
+fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x);
(*possibility to print a given term for debugging purposes*)
@@ -460,7 +460,7 @@
(*mutate origTerm iter times by only exchanging subterms*)
fun mutate_exc origTerm commutatives iter =
- mutate 0 origTerm (theory "Main") commutatives [] iter;
+ mutate 0 origTerm @{theory Main} commutatives [] iter;
(*mutate origTerm iter times by only inserting signature functions*)