--- a/src/Pure/Isar/attrib.ML Wed Jul 17 09:32:08 2013 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Jul 17 11:38:57 2013 +0200
@@ -252,8 +252,6 @@
local
-val strict_eq_thm = op = o pairself Thm.rep_thm;
-
fun apply_att src (context, th) =
let
val src1 = Args.assignable src;
@@ -275,7 +273,7 @@
(case decls of
[] => [(th, [src'])]
| (th2, srcs2) :: rest =>
- if strict_eq_thm (th, th2)
+ if Thm.eq_thm_strict (th, th2)
then ((th2, src' :: srcs2) :: rest)
else (th, [src']) :: (th2, srcs2) :: rest);
in ((th, NONE), (decls', context')) end
@@ -308,7 +306,7 @@
|>> flat;
val decls' = rev (map (apsnd rev) decls);
val facts' =
- if eq_list (eq_fst strict_eq_thm) (decls', fact') then
+ if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then
[((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
else if null decls' then [((b, []), fact')]
else [(empty_binding, decls'), ((b, []), fact')];
--- a/src/Pure/more_thm.ML Wed Jul 17 09:32:08 2013 +0200
+++ b/src/Pure/more_thm.ML Wed Jul 17 11:38:57 2013 +0200
@@ -39,6 +39,7 @@
val eq_thm: thm * thm -> bool
val eq_thm_thy: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
+ val eq_thm_strict: thm * thm -> bool
val equiv_thm: thm * thm -> bool
val class_triv: theory -> class -> thm
val of_sort: ctyp * sort -> thm list
@@ -192,6 +193,11 @@
val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
+fun eq_thm_strict ths =
+ eq_thm_thy ths andalso eq_thm ths andalso
+ let val (rep1, rep2) = pairself Thm.rep_thm ths
+ in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end;
+
(* pattern equivalence *)