moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
--- a/src/FOLP/simp.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/FOLP/simp.ML Mon Feb 26 23:18:24 2007 +0100
@@ -64,7 +64,7 @@
(*** Indexing and filtering of theorems ***)
-fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Drule.eq_thm_prop (th1, th2);
+fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2);
(*insert a thm in a discrimination net by its lhs*)
fun lhs_insert_thm (th,net) =
@@ -248,7 +248,7 @@
(*insert a thm in a thm net*)
fun insert_thm_warn th net =
- Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
+ Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
handle Net.INSERT =>
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
net);
@@ -274,7 +274,7 @@
(*delete a thm from a thm net*)
fun delete_thm_warn th net =
- Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
+ Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
handle Net.DELETE =>
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;
net);
@@ -282,7 +282,7 @@
val delete_thms = fold_rev delete_thm_warn;
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
-let val congs' = fold (remove Drule.eq_thm_prop) thms congs
+let val congs' = fold (remove Thm.eq_thm_prop) thms congs
in SS{auto_tac=auto_tac, congs= congs',
cong_net= delete_thms (map mk_trans thms) cong_net,
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
@@ -290,7 +290,7 @@
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
let fun find((p as (th,ths))::ps',ps) =
- if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
+ if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
| find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
print_thm thm;
([],simps'))
--- a/src/HOL/Library/EfficientNat.thy Mon Feb 26 21:34:16 2007 +0100
+++ b/src/HOL/Library/EfficientNat.thy Mon Feb 26 23:18:24 2007 +0100
@@ -261,7 +261,7 @@
[] => NONE
| thps =>
let val (ths1, ths2) = split_list thps
- in SOME (subtract eq_thm (th :: ths1) thms @ ths2) end
+ in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
end
in
case get_first mk_thms eqs of
--- a/src/HOL/Tools/inductive_codegen.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Feb 26 23:18:24 2007 +0100
@@ -31,7 +31,7 @@
fun merge_rules tabs =
Symtab.join (fn _ => fn (ths, ths') =>
- gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths') tabs;
+ gen_merge_lists (Thm.eq_thm_prop o pairself fst) ths ths') tabs;
structure CodegenData = TheoryDataFun
(struct
--- a/src/HOL/Tools/meson.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/HOL/Tools/meson.ML Mon Feb 26 23:18:24 2007 +0100
@@ -498,7 +498,7 @@
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
fun make_horns ths =
name_thms "Horn#"
- (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
+ (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
(*Could simply use nprems_of, which would count remaining subgoals -- no
discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
@@ -609,7 +609,7 @@
fun make_meta_clauses ths =
name_thms "MClause#"
- (distinct Drule.eq_thm_prop (map make_meta_clause ths));
+ (distinct Thm.eq_thm_prop (map make_meta_clause ths));
(*Permute a rule's premises to move the i-th premise to the last position.*)
fun make_last i th =
--- a/src/HOL/Tools/recdef_package.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/HOL/Tools/recdef_package.ML Mon Feb 26 23:18:24 2007 +0100
@@ -109,7 +109,7 @@
(tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
(Symtab.merge (K true) (tab1, tab2),
mk_hints (Drule.merge_rules (simps1, simps2),
- AList.merge (op =) eq_thm (congs1, congs2),
+ AList.merge (op =) Thm.eq_thm (congs1, congs2),
Drule.merge_rules (wfs1, wfs2)));
fun print thy (tab, hints) =
--- a/src/HOL/Tools/recfun_codegen.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Mon Feb 26 23:18:24 2007 +0100
@@ -24,7 +24,7 @@
val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ = Symtab.merge_list (Drule.eq_thm_prop o pairself fst);
+ fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
fun print _ _ = ();
end);
@@ -56,7 +56,7 @@
in case Symtab.lookup tab s of
NONE => thy
| SOME thms =>
- RecCodegenData.put (Symtab.update (s, remove (eq_thm o apsnd fst) thm thms) tab) thy
+ RecCodegenData.put (Symtab.update (s, remove (Thm.eq_thm o apsnd fst) thm thms) tab) thy
end handle TERM _ => (warn thm; thy);
val del = Thm.declaration_attribute
--- a/src/HOL/Tools/res_axioms.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/HOL/Tools/res_axioms.ML Mon Feb 26 23:18:24 2007 +0100
@@ -51,7 +51,7 @@
fun seed th net =
let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th)
val t = Logic.legacy_varify (term_of ct)
- in Net.insert_term eq_thm (t, th) net end;
+ in Net.insert_term Thm.eq_thm (t, th) net end;
val abstraction_cache = ref
(seed (thm"ATP_Linkup.I_simp")
@@ -492,7 +492,7 @@
change clause_cache (Symtab.update (name, (th, cls)));
(cls,thy')))
| SOME (th',cls) =>
- if eq_thm(th,th') then (cls,thy)
+ if Thm.eq_thm(th,th') then (cls,thy)
else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name);
Output.debug (fn () => string_of_thm th);
Output.debug (fn () => string_of_thm th');
@@ -510,7 +510,7 @@
change clause_cache (Symtab.update (s, (th, cls))); cls
end
| SOME(th',cls) =>
- if eq_thm(th,th') then cls
+ if Thm.eq_thm(th,th') then cls
else
(Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name);
Output.debug (fn () => string_of_thm th);
@@ -601,7 +601,7 @@
case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of
NONE => skolem_thm th
| SOME (th',cls) =>
- if eq_thm(th,th') then cls else skolem_thm th;
+ if Thm.eq_thm(th,th') then cls else skolem_thm th;
fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
--- a/src/Provers/classical.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Provers/classical.ML Mon Feb 26 23:18:24 2007 +0100
@@ -195,7 +195,7 @@
else all_tac))
|> Seq.hd
|> Drule.zero_var_indexes;
- in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
+ in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
else rule;
@@ -342,8 +342,8 @@
fun delete x = delete_tagged_list (joinrules x);
fun delete' x = delete_tagged_list (joinrules' x);
-val mem_thm = member Drule.eq_thm_prop
-and rem_thm = remove Drule.eq_thm_prop;
+val mem_thm = member Thm.eq_thm_prop
+and rem_thm = remove Thm.eq_thm_prop;
(*Warn if the rule is already present ELSEWHERE in the claset. The addition
is still allowed.*)
--- a/src/Pure/Isar/context_rules.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Isar/context_rules.ML Mon Feb 26 23:18:24 2007 +0100
@@ -85,7 +85,7 @@
fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
let
- fun eq_th (_, (_, th')) = Drule.eq_thm_prop (th, th');
+ fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
in
if not (exists eq_th rules) then rs
@@ -106,7 +106,7 @@
val wrappers =
(Library.merge (eq_snd (op =)) (ws1, ws2), Library.merge (eq_snd (op =)) (ws1', ws2'));
val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
- k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
+ k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
val next = ~ (length rules);
val netpairs = fold (fn (n, (w, ((i, b), th))) =>
nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
--- a/src/Pure/Isar/find_theorems.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Isar/find_theorems.ML Mon Feb 26 23:18:24 2007 +0100
@@ -227,7 +227,7 @@
in
map (`(eval_filters filters)) thms
|> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
- |> sort thm_ord |> map #2
+ |> sort thm_ord |> map #2
end;
end;
@@ -236,32 +236,30 @@
(* removing duplicates, preferring nicer names *)
fun rem_thm_dups xs =
- let
- fun nicer (Fact x) (Fact y) = size x <= size y
- | nicer (Fact _) _ = true
- | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
- | nicer (PureThy.Name _) (Fact _) = false
- | nicer (PureThy.Name _) _ = true
- | nicer (NameSelection (x,_)) (NameSelection (y,_)) = size x <= size y
- | nicer (NameSelection _) _ = false;
+ let
+ fun nicer (Fact x) (Fact y) = size x <= size y
+ | nicer (Fact _) _ = true
+ | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
+ | nicer (PureThy.Name _) (Fact _) = false
+ | nicer (PureThy.Name _) _ = true
+ | nicer (NameSelection (x, _)) (NameSelection (y, _)) = size x <= size y
+ | nicer (NameSelection _) _ = false;
- fun is_in [] _ = NONE
- | is_in ((n,t) :: xs) t' = if eq_thm (t, t')
- then SOME (n,t)
- else is_in xs t';
+ fun is_in [] _ = NONE
+ | is_in ((n, t) :: xs) t' =
+ if Thm.eq_thm (t, t') then SOME (n, t) else is_in xs t';
- fun eq ((_,t1),(_,t2)) = eq_thm (t1,t2)
+ fun eq ((_, t1), (_, t2)) = Thm.eq_thm (t1, t2);
- fun rem_d (rev_seen, []) = rev rev_seen
- | rem_d (rev_seen, (x as (n',t')) :: xs) =
- case is_in rev_seen t' of
- NONE => rem_d (x::rev_seen, xs)
- | SOME (n,t) => if nicer n n'
- then rem_d (rev_seen, xs)
- else rem_d (x::remove eq (n,t) rev_seen,xs)
-
- in rem_d ([], xs) end;
-
+ fun rem_d (rev_seen, []) = rev rev_seen
+ | rem_d (rev_seen, (x as (n', t')) :: xs) =
+ (case is_in rev_seen t' of
+ NONE => rem_d (x :: rev_seen, xs)
+ | SOME (n, t) =>
+ if nicer n n'
+ then rem_d (rev_seen, xs)
+ else rem_d (x :: remove eq (n, t) rev_seen, xs))
+ in rem_d ([], xs) end;
(* print_theorems *)
@@ -272,7 +270,7 @@
(ProofContext.lthms_containing ctxt spec
|> maps PureThy.selections
|> distinct (fn ((r1, th1), (r2, th2)) =>
- r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
+ r1 = r2 andalso Thm.eq_thm_prop (th1, th2)));
fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
@@ -280,9 +278,10 @@
val filters = map (filter_criterion ctxt opt_goal) criteria;
val raw_matches = all_filters filters (find_thms ctxt ([], []));
- val matches = if rem_dups andalso not (null filters)
- then rem_thm_dups raw_matches
- else raw_matches;
+ val matches =
+ if rem_dups andalso not (null filters)
+ then rem_thm_dups raw_matches
+ else raw_matches;
val len = length matches;
val limit = the_default (! thms_containing_limit) opt_limit;
--- a/src/Pure/Isar/induct_attrib.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Isar/induct_attrib.ML Mon Feb 26 23:18:24 2007 +0100
@@ -83,7 +83,7 @@
val init_rules =
NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
- Drule.eq_thm_prop (th1, th2));
+ Thm.eq_thm_prop (th1, th2));
fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
--- a/src/Pure/Isar/net_rules.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Isar/net_rules.ML Mon Feb 26 23:18:24 2007 +0100
@@ -63,8 +63,8 @@
(* intro/elim rules *)
-val intro = init Drule.eq_thm_prop Thm.concl_of;
-val elim = init Drule.eq_thm_prop Thm.major_prem_of;
+val intro = init Thm.eq_thm_prop Thm.concl_of;
+val elim = init Thm.eq_thm_prop Thm.major_prem_of;
end;
--- a/src/Pure/Proof/extraction.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Proof/extraction.ML Mon Feb 26 23:18:24 2007 +0100
@@ -206,7 +206,7 @@
typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
types = merge_alists types1 types2,
realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
- defs = gen_merge_lists eq_thm defs1 defs2,
+ defs = gen_merge_lists Thm.eq_thm defs1 defs2,
expand = merge_lists expand1 expand2,
prep = (case prep1 of NONE => prep2 | _ => prep1)};
@@ -373,7 +373,7 @@
typeof_eqns = add_rule (([],
Logic.dest_equals (prop_of (Drule.abs_def thm))), typeof_eqns),
types = types,
- realizers = realizers, defs = insert eq_thm thm defs,
+ realizers = realizers, defs = insert Thm.eq_thm thm defs,
expand = expand, prep = prep}
else
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
--- a/src/Pure/Tools/codegen_data.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML Mon Feb 26 23:18:24 2007 +0100
@@ -92,7 +92,7 @@
then (false, xs)
else (true, AList.merge eq_key eq xys);
-val merge_thms = merge' eq_thm;
+val merge_thms = merge' Thm.eq_thm;
fun merge_lthms (r1, r2) =
if Susp.same (r1, r2)
@@ -123,7 +123,7 @@
fun drop thm' = not (matches args (args_of thm'))
orelse (warning ("Dropping redundant defining equation\n" ^ string_of_thm thm'); false);
val (keeps, drops) = List.partition drop sels;
- in (thm :: keeps, dels |> fold (insert eq_thm) drops |> remove eq_thm thm) end;
+ in (thm :: keeps, dels |> fold (insert Thm.eq_thm) drops |> remove Thm.eq_thm thm) end;
fun add_thm thm (sels, dels) =
apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
@@ -136,7 +136,7 @@
fold add_thm (Susp.force lthms) (sels, dels);
fun del_thm thm (sels, dels) =
- (Susp.value (remove eq_thm thm (Susp.force sels)), thm :: dels);
+ (Susp.value (remove Thm.eq_thm thm (Susp.force sels)), thm :: dels);
fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
@@ -145,8 +145,8 @@
val (dels_t, dels) = merge_thms (dels1, dels2);
in if dels_t
then let
- val (_, sels) = merge_thms (Susp.force sels1, subtract eq_thm dels1 (Susp.force sels2))
- val (_, dels) = merge_thms (dels1, subtract eq_thm (Susp.force sels1) dels2)
+ val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm dels1 (Susp.force sels2))
+ val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm (Susp.force sels1) dels2)
in (true, ((lazy o K) sels, dels)) end
else let
val (sels_t, sels) = merge_lthms (sels1, sels2)
@@ -705,10 +705,10 @@
in map_exec_purge (SOME consts) del thy end;
fun add_inline thm thy =
- (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert eq_thm) (CodegenFunc.mk_rew thm)) thy;
+ (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
fun del_inline thm thy =
- (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove eq_thm) (CodegenFunc.mk_rew thm)) thy ;
+ (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy ;
fun add_inline_proc (name, f) =
(map_exec_purge NONE o map_preproc o apfst o apsnd) (AList.update (op =) (name, (serial (), f)));
--- a/src/Pure/Tools/nbe.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Tools/nbe.ML Mon Feb 26 23:18:24 2007 +0100
@@ -35,7 +35,7 @@
val extend = I;
fun merge _ ((pres1,posts1), (pres2,posts2)) =
- (Library.merge eq_thm (pres1,pres2), Library.merge eq_thm (posts1,posts2))
+ (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
fun print _ _ = ()
end);
@@ -44,9 +44,9 @@
let
fun map_data f = Context.mapping (NBE_Rewrite.map f) I;
fun attr_pre (thy, thm) =
- ((map_data o apfst) (insert eq_thm thm) thy, thm)
+ ((map_data o apfst) (insert Thm.eq_thm thm) thy, thm)
fun attr_post (thy, thm) =
- ((map_data o apsnd) (insert eq_thm thm) thy, thm)
+ ((map_data o apsnd) (insert Thm.eq_thm thm) thy, thm)
val attr = Attrib.syntax (Scan.lift (Args.$$$ "pre" >> K attr_pre
|| Args.$$$ "post" >> K attr_post));
in
--- a/src/Pure/drule.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/drule.ML Mon Feb 26 23:18:24 2007 +0100
@@ -59,9 +59,6 @@
val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
val read_instantiate: (string*string)list -> thm -> thm
val cterm_instantiate: (cterm*cterm)list -> thm -> thm
- val eq_thm_thy: thm * thm -> bool
- val eq_thm_prop: thm * thm -> bool
- val equiv_thm: thm * thm -> bool
val size_of_thm: thm -> int
val reflexive_thm: thm
val symmetric_thm: thm
@@ -557,30 +554,21 @@
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
fun tha COMP thb =
- case distinct eq_thm (compose(tha,1,thb)) of
+ case distinct Thm.eq_thm (compose(tha,1,thb)) of
[th] => th
| _ => raise THM("COMP", 1, [tha,thb]);
(** theorem equality **)
-(*True if the two theorems have the same theory.*)
-val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm;
-
-(*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
-val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
-
(*Useful "distance" function for BEST_FIRST*)
val size_of_thm = size_of_term o Thm.full_prop_of;
(*maintain lists of theorems --- preserving canonical order*)
-val del_rule = remove eq_thm_prop;
+val del_rule = remove Thm.eq_thm_prop;
fun add_rule th = cons th o del_rule th;
-val merge_rules = Library.merge eq_thm_prop;
+val merge_rules = Library.merge Thm.eq_thm_prop;
-(*pattern equivalence*)
-fun equiv_thm ths =
- Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
(*** Meta-Rewriting Rules ***)
--- a/src/Pure/meta_simplifier.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/meta_simplifier.ML Mon Feb 26 23:18:24 2007 +0100
@@ -147,7 +147,7 @@
*)
fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
- Drule.eq_thm_prop (thm1, thm2);
+ Thm.eq_thm_prop (thm1, thm2);
(* congruences *)
@@ -155,7 +155,7 @@
type cong = {thm: thm, lhs: cterm};
fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
- Drule.eq_thm_prop (thm1, thm2);
+ Thm.eq_thm_prop (thm1, thm2);
(* simplification sets, procedures, and solvers *)
@@ -238,7 +238,7 @@
fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
- s1 = s2 andalso eq_list eq_thm (ths1, ths2);
+ s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
@@ -789,7 +789,7 @@
loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
val rules' = Net.merge eq_rrule (rules1, rules2);
- val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2;
+ val prems' = gen_merge_lists Thm.eq_thm_prop prems1 prems2;
val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
val weak' = merge (op =) (weak1, weak2);
--- a/src/Pure/old_goals.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/old_goals.ML Mon Feb 26 23:18:24 2007 +0100
@@ -392,9 +392,9 @@
(case Seq.pull(tac th) of
NONE => error"by: tactic failed"
| SOME(th2,ths2) =>
- (if eq_thm(th,th2)
+ (if Thm.eq_thm(th,th2)
then warning "Warning: same as previous level"
- else if eq_thm_thy(th,th2) then ()
+ else if Thm.eq_thm_thy(th,th2) then ()
else warning ("Warning: theory of proof state has changed" ^
thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
((th2,ths2)::(th,ths)::pairs)));
@@ -414,9 +414,9 @@
(case Seq.pull thstr of
NONE => (writeln"Going back a level..."; backtrack pairs)
| SOME(th2,thstr2) =>
- (if eq_thm(th,th2)
+ (if Thm.eq_thm(th,th2)
then warning "Warning: same as previous choice at this level"
- else if eq_thm_thy(th,th2) then ()
+ else if Thm.eq_thm_thy(th,th2) then ()
else warning "Warning: theory of proof state has changed";
(th2,thstr2)::pairs));
--- a/src/Pure/search.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/search.ML Mon Feb 26 23:18:24 2007 +0100
@@ -64,7 +64,7 @@
case Seq.pull q of
NONE => depth used qs
| SOME(st,stq) =>
- if satp st andalso not (member eq_thm used st)
+ if satp st andalso not (member Thm.eq_thm used st)
then SOME(st, Seq.make
(fn()=> depth (st::used) (stq::qs)))
else depth used (tac st :: stq :: qs)
@@ -211,7 +211,7 @@
(*Check for and delete duplicate proof states*)
fun deleteAllMin prf heap =
if ThmHeap.is_empty heap then heap
- else if eq_thm (prf, #2 (ThmHeap.min heap))
+ else if Thm.eq_thm (prf, #2 (ThmHeap.min heap))
then deleteAllMin prf (ThmHeap.delete_min heap)
else heap;
@@ -269,7 +269,7 @@
fun insert_with_level (lnth: int*int*thm, []) = [lnth]
| insert_with_level ((l,m,th), (l',n,th')::nths) =
if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
- else if n=m andalso eq_thm(th,th')
+ else if n=m andalso Thm.eq_thm(th,th')
then (l',n,th')::nths
else (l,m,th)::(l',n,th')::nths;
--- a/src/Pure/tactic.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/tactic.ML Mon Feb 26 23:18:24 2007 +0100
@@ -421,7 +421,7 @@
foldr insert_tagged_brl netpair (taglist 1 brls);
(*delete one kbrl from the pair of nets*)
-fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
+fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
(if eres then
--- a/src/Pure/tctical.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/tctical.ML Mon Feb 26 23:18:24 2007 +0100
@@ -160,7 +160,7 @@
| evyBack ((st',q,tacs)::trail) =
case Seq.pull q of
NONE => evyBack trail
- | SOME(st,q') => if eq_thm (st',st)
+ | SOME(st,q') => if Thm.eq_thm (st',st)
then evyBack ((st',q',tacs)::trail)
else EVY ((st,q',tacs)::trail, tacs) st
in
@@ -302,7 +302,7 @@
(*Accept only next states that change the theorem's prop field
(changes to signature, hyps, etc. don't count)*)
fun CHANGED_PROP tac st =
- let fun diff st' = not (Drule.eq_thm_prop (st, st'));
+ let fun diff st' = not (Thm.eq_thm_prop (st, st'));
in Seq.filter diff (tac st) end;
--- a/src/Sequents/prover.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Sequents/prover.ML Mon Feb 26 23:18:24 2007 +0100
@@ -32,15 +32,15 @@
dups);
fun (Pack(safes,unsafes)) add_safes ths =
- let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
- val ths' = subtract Drule.eq_thm_prop dups ths
+ let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes))
+ val ths' = subtract Thm.eq_thm_prop dups ths
in
Pack(sort (make_ord less) (ths'@safes), unsafes)
end;
fun (Pack(safes,unsafes)) add_unsafes ths =
- let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
- val ths' = subtract Drule.eq_thm_prop dups ths
+ let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,unsafes))
+ val ths' = subtract Thm.eq_thm_prop dups ths
in
Pack(safes, sort (make_ord less) (ths'@unsafes))
end;
--- a/src/ZF/Tools/typechk.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/ZF/Tools/typechk.ML Mon Feb 26 23:18:24 2007 +0100
@@ -27,16 +27,16 @@
net: thm Net.net}; (*discrimination net of the same rules*)
fun add_rule th (tcs as TC {rules, net}) =
- if member Drule.eq_thm_prop rules th then
+ if member Thm.eq_thm_prop rules th then
(warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
else
TC {rules = th :: rules,
net = Net.insert_term (K false) (Thm.concl_of th, th) net};
fun del_rule th (tcs as TC {rules, net}) =
- if member Drule.eq_thm_prop rules th then
- TC {net = Net.delete_term Drule.eq_thm_prop (Thm.concl_of th, th) net,
- rules = remove Drule.eq_thm_prop th rules}
+ if member Thm.eq_thm_prop rules th then
+ TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
+ rules = remove Thm.eq_thm_prop th rules}
else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
@@ -51,7 +51,7 @@
fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
TC {rules = Drule.merge_rules (rules, rules'),
- net = Net.merge Drule.eq_thm_prop (net, net')};
+ net = Net.merge Thm.eq_thm_prop (net, net')};
fun print context (TC {rules, ...}) =
Pretty.writeln (Pretty.big_list "type-checking rules:"