tuned

--- a/src/HOL/ex/Computations.thy	Sat Feb 04 21:15:11 2017 +0100
+++ b/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:30 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>Simple example for computations generated by the code generator\<close>
 
 theory Computations
-  imports Nat Fun_Def Num Code_Numeral
+  imports "../Nat" "../Fun_Def" "../Num" "../Code_Numeral"
 begin
 
 fun even :: "nat \<Rightarrow> bool"
@@ -37,7 +37,7 @@
 
 val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
   HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool }
-  (K I)
+  (K I);
 
 end
 \<close>

--- a/src/Tools/Code/code_runtime.ML	Sat Feb 04 21:15:11 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:30 2017 +0100
@@ -28,14 +28,14 @@
     -> Proof.context -> term -> 'a Exn.result
   val dynamic_holds_conv: Proof.context -> conv
   val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
-  val mount_computation: Proof.context -> (string * typ) list -> typ
-    -> (term -> 'b) -> ((term -> term) -> 'b -> 'a) -> Proof.context -> term -> 'a
   val code_reflect: (string * string list option) list -> string list -> string
     -> string option -> theory -> theory
   datatype truth = Holds
   val put_truth: (unit -> truth) -> Proof.context -> Proof.context
+  val mount_computation: Proof.context -> (string * typ) list -> typ
+    -> (term -> 'ml) -> ((term -> term) -> 'ml -> 'a) -> Proof.context -> term -> 'a
+  val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
   val trace: bool Config.T
-  val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
 end;
 
 structure Code_Runtime : CODE_RUNTIME =
@@ -48,8 +48,9 @@
 (* technical prerequisites *)
 
 val thisN = "Code_Runtime";
-val truthN = Long_Name.append thisN "truth";
-val HoldsN = Long_Name.append thisN "Holds";
+val prefix_this = Long_Name.append thisN;
+val truthN = prefix_this "truth";
+val HoldsN = prefix_this "Holds";
 
 val target = "Eval";
 
@@ -151,7 +152,7 @@
   fun init _ = empty;
 );
 val put_truth = Truth_Result.put;
-val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append thisN "put_truth");
+val truth_cookie = (Truth_Result.get, put_truth, prefix_this "put_truth");
 
 local
 
@@ -349,13 +350,15 @@
         ] |> rpair of_term_names
       end;
 
+fun checked_computation cTs T raw_computation ctxt =
+  check_typ ctxt T
+  #> reject_vars ctxt
+  #> check_computation_input ctxt cTs
+  #> raw_computation;
+
 fun mount_computation ctxt cTs T raw_computation lift_postproc =
   Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
-    (fn _ => fn ctxt' =>
-      check_typ ctxt' T
-      #> reject_vars ctxt'
-      #> check_computation_input ctxt' cTs
-      #> raw_computation);
+    (K (checked_computation cTs T raw_computation));
 
 
 (** variants of universal runtime code generation **)
@@ -433,7 +436,7 @@
 
 (** code and computation antiquotations **)
 
-val mount_computationN = Long_Name.append thisN "mount_computation";
+val mount_computationN = prefix_this "mount_computation";
 
 local
 
@@ -526,14 +529,14 @@
 fun ml_computation_antiq (raw_ts, raw_T) ctxt =
   let
     val ts = map (Syntax.check_term ctxt) raw_ts;
+    val cTs = (fold o fold_aterms)
+      (fn (t as Const (cT as (_, T))) =>
+        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
+        else insert (op =) cT | _ => I) ts [];
     val T = Syntax.check_typ ctxt raw_T;
     val _ = if not (monomorphic T)
       then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
       else ();
-    val cTs = (fold o fold_aterms)
-      (fn (t as Const (cT as (_, T))) =>
-        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
-        else insert (op =) cT | _ => I) ts [];
   in (print_computation ctxt T, register_computation cTs T ctxt) end;
 
 end; (*local*)
@@ -634,7 +637,8 @@
 
 val _ =
   Theory.setup (ML_Antiquotation.declaration @{binding computation}
-    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ) (fn _ => ml_computation_antiq));
+    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
+       (fn _ => ml_computation_antiq));
 
 local