# HG changeset patch # User wenzelm # Date 1172528304 -3600 # Node ID 26ead7ed4f4bd3270939db6a726e71f987398d5c # Parent 94a794672c8b3f9b6f7cf89dd0d0d773d893a8a6 moved eq_thm etc. to structure Thm in Pure/more_thm.ML; diff -r 94a794672c8b -r 26ead7ed4f4b src/FOLP/simp.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')) diff -r 94a794672c8b -r 26ead7ed4f4b src/HOL/Library/EfficientNat.thy --- 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 diff -r 94a794672c8b -r 26ead7ed4f4b src/HOL/Tools/inductive_codegen.ML --- 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 diff -r 94a794672c8b -r 26ead7ed4f4b src/HOL/Tools/meson.ML --- 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 = diff -r 94a794672c8b -r 26ead7ed4f4b src/HOL/Tools/recdef_package.ML --- 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) = diff -r 94a794672c8b -r 26ead7ed4f4b src/HOL/Tools/recfun_codegen.ML --- 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 diff -r 94a794672c8b -r 26ead7ed4f4b src/HOL/Tools/res_axioms.ML --- 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); diff -r 94a794672c8b -r 26ead7ed4f4b src/Provers/classical.ML --- 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.*) diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/Isar/context_rules.ML --- 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)))) diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/Isar/find_theorems.ML --- 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; diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/Isar/induct_attrib.ML --- 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); diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/Isar/net_rules.ML --- 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; diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/Proof/extraction.ML --- 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, diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/Tools/codegen_data.ML --- 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))); diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/Tools/nbe.ML --- 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 diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/drule.ML --- 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 ***) diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/meta_simplifier.ML --- 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); diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/old_goals.ML --- 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)); diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/search.ML --- 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 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; diff -r 94a794672c8b -r 26ead7ed4f4b src/Sequents/prover.ML --- 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; diff -r 94a794672c8b -r 26ead7ed4f4b src/ZF/Tools/typechk.ML --- 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:"