--- a/src/HOL/Code_Evaluation.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Code_Evaluation.thy Sat May 25 15:37:53 2013 +0200
@@ -144,15 +144,15 @@
subsubsection {* Obfuscation *}
print_translation {*
-let
- val term = Const ("<TERM>", dummyT);
- fun tr1' [_, _] = term;
- fun tr2' [] = term;
-in
- [(@{const_syntax Const}, tr1'),
+ let
+ val term = Const ("<TERM>", dummyT);
+ fun tr1' _ [_, _] = term;
+ fun tr2' _ [] = term;
+ in
+ [(@{const_syntax Const}, tr1'),
(@{const_syntax App}, tr1'),
(@{const_syntax dummy_term}, tr2')]
-end
+ end
*}