# HG changeset patch
# User wenzelm
# Date 1374053937 -7200
# Node ID fb028440473e863c129a3b4915ea6abfd3761d17
# Parent  77146b576ac7ecdebd5d2b72a8b14743d9008a95
more official Thm.eq_thm_strict, without demanding ML equality type;

diff -r 77146b576ac7 -r fb028440473e src/Pure/Isar/attrib.ML
--- 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')];
diff -r 77146b576ac7 -r fb028440473e src/Pure/more_thm.ML
--- 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 *)