--- 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,
--- 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;
--- 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 "")^"]"
--- 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);
--- 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 *)
--- 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')
--- 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 ****)
--- 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);
--- 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