# HG changeset patch
# User haftmann
# Date 1464269270 -7200
# Node ID 3cb84e4469a76de644d2b7673784e911543eff5a
# Parent  ea8540c715813bc73d1e0489a9170bf12d00d3af
clarified names of variants

diff -r ea8540c71581 -r 3cb84e4469a7 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
@@ -200,7 +200,7 @@
       o reject_vars ctxt;
 
 fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
-  Code_Thingol.static_conv ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
+  Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
     K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
 
 end; (*local*)
diff -r ea8540c71581 -r 3cb84e4469a7 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu May 26 15:27:50 2016 +0200
@@ -94,7 +94,7 @@
 (* evaluation with static code context *)
 
 fun static_conv { ctxt, simpset, consts } =
-  Code_Thingol.static_conv_simple { ctxt = ctxt, consts = consts }
+  Code_Thingol.static_conv_isa { ctxt = ctxt, consts = consts }
     (K oo rewrite_modulo ctxt simpset);
 
 fun static_tac { ctxt, simpset, consts } =
diff -r ea8540c71581 -r 3cb84e4469a7 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
@@ -91,11 +91,11 @@
   val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
     -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     -> term -> 'a
-  val static_conv: { ctxt: Proof.context, consts: string list }
+  val static_conv_thingol: { ctxt: Proof.context, consts: string list }
     -> ({ program: program, deps: string list }
       -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> Proof.context -> conv
-  val static_conv_simple: { ctxt: Proof.context, consts: string list }
+  val static_conv_isa: { ctxt: Proof.context, consts: string list }
     -> (program -> Proof.context -> term -> conv)
     -> Proof.context -> conv
   val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list }
@@ -857,7 +857,7 @@
       ensure_value ctxt algebra eqngr t ([], program);
   in subevaluator ctxt t (vs_ty', t') deps end;
 
-fun static_evaluator ctxt evaluator consts { algebra, eqngr } =
+fun static_evaluator_thingol ctxt evaluator consts { algebra, eqngr } =
   let
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr false);
@@ -866,7 +866,7 @@
     val subevaluator = evaluator { program = program, deps = deps };
   in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
 
-fun static_evaluator_simple ctxt evaluator consts { algebra, eqngr } =
+fun static_evaluator_isa ctxt evaluator consts { algebra, eqngr } =
   let
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr false);
@@ -874,14 +874,14 @@
       invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
   in evaluator (program: program) end;
 
-fun static_conv (ctxt_consts as { ctxt, consts }) conv =
-  Code_Preproc.static_conv ctxt_consts (static_evaluator ctxt (K oo conv) consts);
+fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv =
+  Code_Preproc.static_conv ctxt_consts (static_evaluator_thingol ctxt (K oo conv) consts);
 
-fun static_conv_simple (ctxt_consts as { ctxt, consts }) conv =
-  Code_Preproc.static_conv ctxt_consts (static_evaluator_simple ctxt conv consts);
+fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv =
+  Code_Preproc.static_conv ctxt_consts (static_evaluator_isa ctxt conv consts);
 
 fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator =
-  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator ctxt evaluator consts);
+  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator_thingol ctxt evaluator consts);
 
 
 (** constant expressions **)
diff -r ea8540c71581 -r 3cb84e4469a7 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
@@ -604,7 +604,7 @@
 
 fun static_conv (ctxt_consts as { ctxt, ... }) =
   let
-    val evaluator = Code_Thingol.static_conv ctxt_consts
+    val evaluator = Code_Thingol.static_conv_thingol ctxt_consts
       (fn { program, ... } => oracle (compile true ctxt program));
   in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;