1.1 --- a/src/Pure/Isar/attrib.ML	Wed Jul 17 09:32:08 2013 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Jul 17 11:38:57 2013 +0200
     1.3 @@ -252,8 +252,6 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val strict_eq_thm = op = o pairself Thm.rep_thm;
     1.8 -
     1.9  fun apply_att src (context, th) =
    1.10    let
    1.11      val src1 = Args.assignable src;
    1.12 @@ -275,7 +273,7 @@
    1.13            (case decls of
    1.14              [] => [(th, [src'])]
    1.15            | (th2, srcs2) :: rest =>
    1.16 -              if strict_eq_thm (th, th2)
    1.17 +              if Thm.eq_thm_strict (th, th2)
    1.18                then ((th2, src' :: srcs2) :: rest)
    1.19                else (th, [src']) :: (th2, srcs2) :: rest);
    1.20        in ((th, NONE), (decls', context')) end
    1.21 @@ -308,7 +306,7 @@
    1.22            |>> flat;
    1.23          val decls' = rev (map (apsnd rev) decls);
    1.24          val facts' =
    1.25 -          if eq_list (eq_fst strict_eq_thm) (decls', fact') then
    1.26 +          if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then
    1.27              [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
    1.28            else if null decls' then [((b, []), fact')]
    1.29            else [(empty_binding, decls'), ((b, []), fact')];

     2.1 --- a/src/Pure/more_thm.ML	Wed Jul 17 09:32:08 2013 +0200
     2.2 +++ b/src/Pure/more_thm.ML	Wed Jul 17 11:38:57 2013 +0200
     2.3 @@ -39,6 +39,7 @@
     2.4    val eq_thm: thm * thm -> bool
     2.5    val eq_thm_thy: thm * thm -> bool
     2.6    val eq_thm_prop: thm * thm -> bool
     2.7 +  val eq_thm_strict: thm * thm -> bool
     2.8    val equiv_thm: thm * thm -> bool
     2.9    val class_triv: theory -> class -> thm
    2.10    val of_sort: ctyp * sort -> thm list
    2.11 @@ -192,6 +193,11 @@
    2.12  val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
    2.13  val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
    2.14  
    2.15 +fun eq_thm_strict ths =
    2.16 +  eq_thm_thy ths andalso eq_thm ths andalso
    2.17 +    let val (rep1, rep2) = pairself Thm.rep_thm ths
    2.18 +    in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end;
    2.19 +
    2.20  
    2.21  (* pattern equivalence *)
    2.22