--- a/src/Pure/Isar/code.ML Sat Jun 28 22:13:21 2014 +0200
+++ b/src/Pure/Isar/code.ML Sat Jun 28 22:13:23 2014 +0200
@@ -891,7 +891,7 @@
end;
-(* code certificate access *)
+(* code certificate access with preprocessing *)
fun retrieve_raw thy c =
Symtab.lookup ((the_functions o the_exec) thy) c
@@ -918,7 +918,7 @@
end;
fun cert_of_eqns_preprocess ctxt functrans c =
- perhaps (perhaps_loop (perhaps_apply functrans))
+ (perhaps o perhaps_loop o perhaps_apply) functrans
#> (map o apfst) (preprocess eqn_conv ctxt)
#> cert_of_eqns ctxt c;