# HG changeset patch
# User wenzelm
# Date 1147367971 -7200
# Node ID 7cb4b67d4b979a1264261009dbbbcba94ebd2d1d
# Parent  2545e8ab59a5c7eca9a8551794722fd5d561dbbf
avoid raw equality on type thm;

diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Thu May 11 19:19:31 2006 +0200
@@ -281,8 +281,8 @@
 
 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
   during re-arrangement*)
-val non_add_bin_simps = 
-    bin_simps \\ [add_number_of_left, number_of_add RS sym];
+val non_add_bin_simps =
+  subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] bin_simps;
 
 (*To evaluate binary negations of coefficients*)
 val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu May 11 19:19:31 2006 +0200
@@ -208,7 +208,7 @@
             (Thm.forall_intr (cert v) th'))
         in
           remove_suc_clause thy (map (fn th''' =>
-            if th''' = th then th'' else th''') thms)
+            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
         end
   end;
 
diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu May 11 19:19:31 2006 +0200
@@ -131,10 +131,10 @@
 fun get_assoc_snds [] xs assocs= assocs
 |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
 
-fun add_if_not_inlist [] xs newlist = newlist
-|   add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
-                                      add_if_not_inlist ys xs (y::newlist)
-                                        else add_if_not_inlist ys xs (newlist)
+fun add_if_not_inlist eq [] xs newlist = newlist
+|   add_if_not_inlist eq (y::ys) xs newlist =
+    if not (member eq xs y) then add_if_not_inlist eq ys xs (y::newlist)
+    else add_if_not_inlist eq ys xs newlist
 
 (*Flattens a list of list of strings to one string*)
 fun onestr ls = String.concat (map String.concat ls);
@@ -245,9 +245,9 @@
      val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
 
      (* get list of extra axioms as thms with their variables *)
-     val extra_metas = add_if_not_inlist metas ax_metas []
+     val extra_metas = add_if_not_inlist Thm.eq_thm metas ax_metas []
      val extra_vars = map thm_vars extra_metas
-     val extra_with_vars = if (not (extra_metas = []) ) 
+     val extra_with_vars = if not (null extra_metas)
 			   then ListPair.zip (extra_metas,extra_vars)
 			   else []
  in
@@ -339,7 +339,7 @@
       val num_cls_vars =  map (addvars vars) numcls_strs;
       val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
       
-      val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars))
+      val extra_nums = if not (null extra_with_vars) then (1 upto (length extra_with_vars))
                        else []
       val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
       val frees_str = "["^(thmvars_to_string frees "")^"]"
diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu May 11 19:19:31 2006 +0200
@@ -108,7 +108,7 @@
   val empty = ("", Symtab.empty);
   val copy = I;
   val extend = I;
-  fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (op =) (tab1, tab2))
+  fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (K true) (tab1, tab2))
 
   fun print _ _ = ();
 end);
diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu May 11 19:19:31 2006 +0200
@@ -162,8 +162,8 @@
 
 (* congruence rules *)
 
-val cong_add = Thm.declaration_attribute (map_fundef_congs o cons o safe_mk_meta_eq);
-val cong_del = Thm.declaration_attribute (map_fundef_congs o remove (op =) o safe_mk_meta_eq);
+val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
 
 
 (* setup *)
diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu May 11 19:19:31 2006 +0200
@@ -436,7 +436,7 @@
     (** add realizers to theory **)
 
     val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth
-      (#intrs ind_info, find_index_eq r intrs)) rs) rss);
+      (#intrs ind_info, find_index (fn th => eq_thm (th, r)) intrs)) rs) rss);
     val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
     val thy5 = Extraction.add_realizers_i
       (map (mk_realizer thy4 vs params')
diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu May 11 19:19:31 2006 +0200
@@ -269,9 +269,7 @@
 
 fun cnf_hyps_thms ctxt = 
     let val ths = ProofContext.prems_of ctxt
-    in
-	ResClause.union_all (map ResAxioms.skolem_thm ths)
-    end;
+    in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
 
 
 (**** write to files ****)
diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Thu May 11 19:19:31 2006 +0200
@@ -72,6 +72,7 @@
 
 (* theory data *)
 
+(* FIXME self-descriptive record type *)
 type typedef_info = (typ * typ * string * string) * (thm option * thm * thm);
 
 structure TypedefData = TheoryDataFun
@@ -81,7 +82,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs;
+  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   fun print _ _ = ();
 end);
 
diff -r 2545e8ab59a5 -r 7cb4b67d4b97 src/Provers/order.ML
--- a/src/Provers/order.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/Provers/order.ML	Thu May 11 19:19:31 2006 +0200
@@ -734,7 +734,7 @@
 in
   (* looking for x <= y: any path from x to y is sufficient *)
   case subgoal of (Le (x, y, _)) => (
-  if sccGraph = [] then raise Cannot else ( 
+  if null sccGraph then raise Cannot else ( 
    let 
     val xi = getIndex x ntc
     val yi = getIndex y ntc
@@ -758,7 +758,7 @@
  (* looking for x < y: particular path required, which is not necessarily
     found by normal dfs *)
  |   (Less (x, y, _)) => (
-  if sccGraph = [] then raise Cannot else (
+  if null sccGraph then raise Cannot else (
    let 
     val xi = getIndex x ntc
     val yi = getIndex y ntc
@@ -780,9 +780,9 @@
  )
 | (NotEq (x, y, _)) => (
   (* if there aren't any edges that are candidate for a ~= raise Cannot *)
-  if neqE = [] then raise Cannot
+  if null neqE then raise Cannot
   (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
-  else if sccSubgraphs = [] then (
+  else if null sccSubgraphs then (
      (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
        ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
           if  (x aconv x' andalso y aconv y') then p