--- a/src/Pure/Isar/attrib.ML Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Mar 14 10:08:36 2014 +0100
@@ -213,7 +213,7 @@
fun gen_thm pick = Scan.depend (fn context =>
let
- val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
+ val get = Proof_Context.get_fact_generic context;
val get_fact = get o Facts.Fact;
fun get_named pos name = get (Facts.Named ((name, pos), NONE));
in
@@ -249,6 +249,8 @@
(** partial evaluation -- observing rule/declaration/mixed attributes **)
+(*NB: result length may change due to rearrangement of symbolic expression*)
+
local
fun apply_att src (context, th) =