--- a/src/HOL/Eisbach/method_closure.ML Tue Dec 22 10:58:05 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Tue Dec 22 11:25:21 2015 +0100
@@ -147,10 +147,6 @@
in (named_thm, parser) end;
-fun instantiate_text env text =
- let val morphism = Morphism.term_morphism "instantiate_text" (Envir.norm_term env);
- in (Method.map_source o map) (Token.transform morphism) text end;
-
fun evaluate_dynamic_thm ctxt name =
(case try (Named_Theorems.get ctxt) name of
SOME thms => thms
@@ -166,11 +162,11 @@
Method.RUNTIME (fn st => Method.evaluate (evaluate_named_theorems ctxt' text) ctxt' facts st)
end;
-fun evaluate_method_def fix_env raw_text ctxt =
+fun method_instantiate env text =
let
- val text = raw_text
- |> instantiate_text fix_env;
- in method_evaluate text ctxt end;
+ val morphism = Morphism.term_morphism "instantiate_text" (Envir.norm_term env);
+ val text' = (Method.map_source o map) (Token.transform morphism) text;
+ in method_evaluate text' end;
fun setup_local_method binding lthy =
let
@@ -236,9 +232,9 @@
val setup_ctxt = fold add_thms attribs
#> fold update_dynamic_method (hmethods ~~ methods)
- #> put_recursive_method (fn fixes => evaluate_method_def (match fixes) text);
+ #> put_recursive_method (fn xs => method_instantiate (match xs) text);
in
- fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
+ fn ctxt => method_instantiate (match fixes) text (setup_ctxt ctxt)
end;
@@ -290,7 +286,7 @@
val term_args' = map (Morphism.term morphism) term_args;
fun real_exec ts ctxt =
- evaluate_method_def (match_term_args ctxt term_args' ts) text' ctxt;
+ method_instantiate (match_term_args ctxt term_args' ts) text' ctxt;
val real_parser =
parser term_args' (fn (fixes, decl) => fn ctxt =>
real_exec fixes (put_recursive_method real_exec (decl ctxt)));