--- a/src/Pure/Isar/token.ML Wed Sep 02 11:36:40 2015 +0200
+++ b/src/Pure/Isar/token.ML Wed Sep 02 13:26:29 2015 +0200
@@ -77,6 +77,8 @@
val map_values: (value -> value) -> src -> src
val declare_maxidx: T -> Proof.context -> Proof.context
val declare_maxidx_src: src -> Proof.context -> Proof.context
+ val map_facts: (thm list -> thm list) -> T -> T
+ val map_facts_src: (thm list -> thm list) -> src -> src
val transform: morphism -> T -> T
val transform_src: morphism -> src -> src
val init_assignable: T -> T
@@ -437,6 +439,17 @@
and declare_maxidx_src src = fold declare_maxidx (args_of_src src);
+(* fact values *)
+
+fun map_facts f =
+ map_value (fn v =>
+ (case v of
+ Source src => Source (map_facts_src f src)
+ | Fact (a, ths) => Fact (a, f ths)
+ | _ => v))
+and map_facts_src f = map_args (map_facts f);
+
+
(* transform *)
fun transform phi =