# HG changeset patch
# User wenzelm
# Date 1449691845 -3600
# Node ID e65344e3eeb5685ae79640f223338afc7e398b04
# Parent  7e020220561a320ad98bc7abd50e1f562631265e
tuned signature;

diff -r 7e020220561a -r e65344e3eeb5 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Wed Dec 09 20:58:09 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Wed Dec 09 21:10:45 2015 +0100
@@ -210,10 +210,8 @@
 
 
 fun evaluate_named_theorems ctxt =
-  (Method.map_source o map o Token.map_nested_values)
-    (fn Token.Fact (SOME name, _) =>
-          Token.Fact (SOME name, evaluate_dynamic_thm ctxt name)
-      | x => x);
+  (Method.map_source o map o Token.map_facts)
+    (fn SOME name => K (evaluate_dynamic_thm ctxt name) | NONE => I);
 
 fun method_evaluate text ctxt facts =
   let val ctxt' = Config.put Method.closure false ctxt in
diff -r 7e020220561a -r e65344e3eeb5 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Dec 09 20:58:09 2015 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Dec 09 21:10:45 2015 +0100
@@ -577,7 +577,7 @@
 local
 
 val trim_fact = map Thm.trim_context;
-val trim_srcs = (map o map o Token.map_facts) trim_fact;
+val trim_srcs = (map o map o Token.map_facts) (K trim_fact);
 
 fun trim_context_facts facts = facts |> map (fn ((b, atts), args) =>
   ((b, trim_srcs atts), map (fn (a, more_atts) => (trim_fact a, trim_srcs more_atts)) args));
diff -r 7e020220561a -r e65344e3eeb5 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Dec 09 20:58:09 2015 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 09 21:10:45 2015 +0100
@@ -64,13 +64,11 @@
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
   val get_value: T -> value option
-  val map_value: (value -> value) -> T -> T
   val name_value: name_value -> value
   val get_name: T -> name_value option
   val reports_of_value: T -> Position.report list
-  val map_nested_values: (value -> value) -> T -> T
   val declare_maxidx: T -> Proof.context -> Proof.context
-  val map_facts: (thm list -> thm list) -> T -> T
+  val map_facts: (string option -> thm list -> thm list) -> T -> T
   val transform: morphism -> T -> T
   val init_assignable: T -> T
   val assign: value option -> T -> T
@@ -369,9 +367,6 @@
 fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
   | map_value _ tok = tok;
 
-fun map_nested_values f =
-  map_value (fn Source src => Source (map (map_nested_values f) src) | x => f x);
-
 
 (* name value *)
 
@@ -421,7 +416,7 @@
   map_value (fn v =>
     (case v of
       Source src => Source (map (map_facts f) src)
-    | Fact (a, ths) => Fact (a, f ths)
+    | Fact (a, ths) => Fact (a, f a ths)
     | _ => v));