Fix test_tutorial5 (#565)

Fixes #511.

doc/tutorial/code/DES.cry

@@ -7,12 +7,9 @@ module DES where
 
 import Cipher
 
-// DES API
-DES : Cipher 64 64
-DES = 
-    { encrypt key pt = des pt (expandKey key)
-    , decrypt key ct = des ct (reverse (expandKey key))
-    }
+encrypt key pt = des pt (expandKey key)
+
+decrypt key ct = des ct (reverse (expandKey key))
 
 // Encryption 
 

doc/tutorial/code/des3.saw

@@ -1,26 +1,38 @@
-m <- cryptol_load "DES.cry";
-let enc = {{ m::DES.encrypt }};
-let dec = {{ m::DES.decrypt }};
+import "DES.cry";
 
 print "proving dec_enc...";
-let {{ prop1 key msg = dec key (enc key msg) == msg }};
-dec_enc <- prove_print do { unfolding ["enc", "dec"]; abc; } {{prop1}};
+let prop1 = {{ \key msg -> decrypt key (encrypt key msg) == msg }};
+dec_enc <- prove_print abc {{prop1}};
+
+print dec_enc;
 
 print "proving enc_dec...";
-let {{ prop2 key msg = enc key (dec key msg) == msg }};
-enc_dec <- prove_print do { unfolding ["enc", "dec"]; abc; } {{prop2}};
+let prop2 = {{ \key msg -> encrypt key (decrypt key msg) == msg }};
+enc_dec <- prove_print abc {{prop2}};
 
 print enc_dec;
 
-let ss = addsimp dec_enc (addsimp enc_dec empty_ss);
+let ss = addsimp dec_enc (addsimp enc_dec basic_ss);
 
-let {{ enc3 k1 k2 k3 msg = enc k3 (dec k2 (enc k1 msg)) }};
-let {{ dec3 k1 k2 k3 msg = dec k1 (enc k2 (dec k3 msg)) }};
+let {{ enc3 k1 k2 k3 msg = encrypt k3 (decrypt k2 (encrypt k1 msg)) }};
+let {{ dec3 k1 k2 k3 msg = decrypt k1 (encrypt k2 (decrypt k3 msg)) }};
 
 print "proving dec3_enc3...";
 let {{ prop3 k1 k2 k3 msg = dec3 k1 k2 k3 (enc3 k1 k2 k3 msg) == msg }};
-prove_print do { simplify ss; print_goal; abc; } {{prop3}};
+prove_print do {
+    unfolding ["prop3"];
+    unfolding ["dec3", "enc3"];
+    simplify ss;
+    print_goal;
+    abc;
+} {{prop3}};
 
 print "proving enc3_dec3...";
 let {{ prop4 k1 k2 k3 msg = enc3 k1 k2 k3 (dec3 k1 k2 k3 msg) == msg }};
-prove_print do { simplify ss; print_goal; abc; } {{prop4}};
+prove_print do {
+    unfolding ["prop4"];
+    unfolding ["dec3", "enc3"];
+    simplify ss;
+    print_goal;
+    abc;
+} {{prop4}};