--- a/src/Tools/Code/code_runtime.ML Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Mar 12 21:58:48 2014 +0100
@@ -257,15 +257,12 @@
in
-fun ml_code_antiq context raw_const =
+fun ml_code_antiq raw_const ctxt =
let
- val ctxt = Context.the_proof context;
val thy = Proof_Context.theory_of ctxt;
-
val const = Code.check_const thy raw_const;
val is_first = is_first_occ ctxt;
- val ctxt' = register_const const ctxt;
- in (Context.Proof ctxt', print_code is_first const) end;
+ in (print_code is_first const, register_const const ctxt) end;
end; (*local*)
@@ -356,9 +353,8 @@
(** Isar setup **)
-val _ = Theory.setup
- (ML_Context.add_antiq @{binding code}
- (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)));
+val _ =
+ Theory.setup (ML_Context.antiquotation @{binding code} Args.term (fn _ => ml_code_antiq));
local