1.1 --- a/src/FOLP/simp.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/FOLP/simp.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  (*** Indexing and filtering of theorems ***)
     1.6  
     1.7 -fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Drule.eq_thm_prop (th1, th2);
     1.8 +fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2);
     1.9  
    1.10  (*insert a thm in a discrimination net by its lhs*)
    1.11  fun lhs_insert_thm (th,net) =
    1.12 @@ -248,7 +248,7 @@
    1.13  
    1.14  (*insert a thm in a thm net*)
    1.15  fun insert_thm_warn th net = 
    1.16 -  Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
    1.17 +  Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
    1.18    handle Net.INSERT => 
    1.19      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    1.20       net);
    1.21 @@ -274,7 +274,7 @@
    1.22  
    1.23  (*delete a thm from a thm net*)
    1.24  fun delete_thm_warn th net = 
    1.25 -  Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
    1.26 +  Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
    1.27    handle Net.DELETE => 
    1.28      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
    1.29       net);
    1.30 @@ -282,7 +282,7 @@
    1.31  val delete_thms = fold_rev delete_thm_warn;
    1.32  
    1.33  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.34 -let val congs' = fold (remove Drule.eq_thm_prop) thms congs
    1.35 +let val congs' = fold (remove Thm.eq_thm_prop) thms congs
    1.36  in SS{auto_tac=auto_tac, congs= congs',
    1.37        cong_net= delete_thms (map mk_trans thms) cong_net,
    1.38        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
    1.39 @@ -290,7 +290,7 @@
    1.40  
    1.41  fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.42  let fun find((p as (th,ths))::ps',ps) =
    1.43 -          if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.44 +          if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.45        | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
    1.46                             print_thm thm;
    1.47                             ([],simps'))

     2.1 --- a/src/HOL/Library/EfficientNat.thy	Mon Feb 26 21:34:16 2007 +0100
     2.2 +++ b/src/HOL/Library/EfficientNat.thy	Mon Feb 26 23:18:24 2007 +0100
     2.3 @@ -261,7 +261,7 @@
     2.4              [] => NONE
     2.5            | thps =>
     2.6                let val (ths1, ths2) = split_list thps
     2.7 -              in SOME (subtract eq_thm (th :: ths1) thms @ ths2) end
     2.8 +              in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
     2.9        end
    2.10    in
    2.11      case get_first mk_thms eqs of

     3.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Feb 26 21:34:16 2007 +0100
     3.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Feb 26 23:18:24 2007 +0100
     3.3 @@ -31,7 +31,7 @@
     3.4  
     3.5  fun merge_rules tabs =
     3.6    Symtab.join (fn _ => fn (ths, ths') =>
     3.7 -    gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths') tabs;
     3.8 +    gen_merge_lists (Thm.eq_thm_prop o pairself fst) ths ths') tabs;
     3.9  
    3.10  structure CodegenData = TheoryDataFun
    3.11  (struct

     4.1 --- a/src/HOL/Tools/meson.ML	Mon Feb 26 21:34:16 2007 +0100
     4.2 +++ b/src/HOL/Tools/meson.ML	Mon Feb 26 23:18:24 2007 +0100
     4.3 @@ -498,7 +498,7 @@
     4.4  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
     4.5  fun make_horns ths =
     4.6      name_thms "Horn#"
     4.7 -      (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
     4.8 +      (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
     4.9  
    4.10  (*Could simply use nprems_of, which would count remaining subgoals -- no
    4.11    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
    4.12 @@ -609,7 +609,7 @@
    4.13    
    4.14  fun make_meta_clauses ths =
    4.15      name_thms "MClause#"
    4.16 -      (distinct Drule.eq_thm_prop (map make_meta_clause ths));
    4.17 +      (distinct Thm.eq_thm_prop (map make_meta_clause ths));
    4.18  
    4.19  (*Permute a rule's premises to move the i-th premise to the last position.*)
    4.20  fun make_last i th =

     5.1 --- a/src/HOL/Tools/recdef_package.ML	Mon Feb 26 21:34:16 2007 +0100
     5.2 +++ b/src/HOL/Tools/recdef_package.ML	Mon Feb 26 23:18:24 2007 +0100
     5.3 @@ -109,7 +109,7 @@
     5.4      (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
     5.5        (Symtab.merge (K true) (tab1, tab2),
     5.6          mk_hints (Drule.merge_rules (simps1, simps2),
     5.7 -          AList.merge (op =) eq_thm (congs1, congs2),
     5.8 +          AList.merge (op =) Thm.eq_thm (congs1, congs2),
     5.9            Drule.merge_rules (wfs1, wfs2)));
    5.10  
    5.11    fun print thy (tab, hints) =

     6.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon Feb 26 21:34:16 2007 +0100
     6.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon Feb 26 23:18:24 2007 +0100
     6.3 @@ -24,7 +24,7 @@
     6.4    val empty = Symtab.empty;
     6.5    val copy = I;
     6.6    val extend = I;
     6.7 -  fun merge _ = Symtab.merge_list (Drule.eq_thm_prop o pairself fst);
     6.8 +  fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
     6.9    fun print _ _ = ();
    6.10  end);
    6.11  
    6.12 @@ -56,7 +56,7 @@
    6.13    in case Symtab.lookup tab s of
    6.14        NONE => thy
    6.15      | SOME thms =>
    6.16 -        RecCodegenData.put (Symtab.update (s, remove (eq_thm o apsnd fst) thm thms) tab) thy
    6.17 +        RecCodegenData.put (Symtab.update (s, remove (Thm.eq_thm o apsnd fst) thm thms) tab) thy
    6.18    end handle TERM _ => (warn thm; thy);
    6.19  
    6.20  val del = Thm.declaration_attribute

     7.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Feb 26 21:34:16 2007 +0100
     7.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Feb 26 23:18:24 2007 +0100
     7.3 @@ -51,7 +51,7 @@
     7.4  fun seed th net =
     7.5    let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th)
     7.6        val t = Logic.legacy_varify (term_of ct)
     7.7 -  in  Net.insert_term eq_thm (t, th) net end;
     7.8 +  in  Net.insert_term Thm.eq_thm (t, th) net end;
     7.9    
    7.10  val abstraction_cache = ref 
    7.11        (seed (thm"ATP_Linkup.I_simp") 
    7.12 @@ -492,7 +492,7 @@
    7.13                    change clause_cache (Symtab.update (name, (th, cls))); 
    7.14                    (cls,thy')))
    7.15      | SOME (th',cls) =>
    7.16 -        if eq_thm(th,th') then (cls,thy)
    7.17 +        if Thm.eq_thm(th,th') then (cls,thy)
    7.18          else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name);
    7.19                Output.debug (fn () => string_of_thm th);
    7.20                Output.debug (fn () => string_of_thm th');
    7.21 @@ -510,7 +510,7 @@
    7.22                       change clause_cache (Symtab.update (s, (th, cls))); cls 
    7.23                    end
    7.24                | SOME(th',cls) =>
    7.25 -                  if eq_thm(th,th') then cls
    7.26 +                  if Thm.eq_thm(th,th') then cls
    7.27                    else
    7.28                      (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name);
    7.29                       Output.debug (fn () => string_of_thm th);
    7.30 @@ -601,7 +601,7 @@
    7.31    case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of
    7.32        NONE => skolem_thm th
    7.33      | SOME (th',cls) =>
    7.34 -        if eq_thm(th,th') then cls else skolem_thm th;
    7.35 +        if Thm.eq_thm(th,th') then cls else skolem_thm th;
    7.36  
    7.37  fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
    7.38  

     8.1 --- a/src/Provers/classical.ML	Mon Feb 26 21:34:16 2007 +0100
     8.2 +++ b/src/Provers/classical.ML	Mon Feb 26 23:18:24 2007 +0100
     8.3 @@ -195,7 +195,7 @@
     8.4            else all_tac))
     8.5          |> Seq.hd
     8.6          |> Drule.zero_var_indexes;
     8.7 -    in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
     8.8 +    in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
     8.9    else rule;
    8.10  
    8.11  
    8.12 @@ -342,8 +342,8 @@
    8.13  fun delete x = delete_tagged_list (joinrules x);
    8.14  fun delete' x = delete_tagged_list (joinrules' x);
    8.15  
    8.16 -val mem_thm = member Drule.eq_thm_prop
    8.17 -and rem_thm = remove Drule.eq_thm_prop;
    8.18 +val mem_thm = member Thm.eq_thm_prop
    8.19 +and rem_thm = remove Thm.eq_thm_prop;
    8.20  
    8.21  (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
    8.22    is still allowed.*)

     9.1 --- a/src/Pure/Isar/context_rules.ML	Mon Feb 26 21:34:16 2007 +0100
     9.2 +++ b/src/Pure/Isar/context_rules.ML	Mon Feb 26 23:18:24 2007 +0100
     9.3 @@ -85,7 +85,7 @@
     9.4  
     9.5  fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
     9.6    let
     9.7 -    fun eq_th (_, (_, th')) = Drule.eq_thm_prop (th, th');
     9.8 +    fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
     9.9      fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
    9.10    in
    9.11      if not (exists eq_th rules) then rs
    9.12 @@ -106,7 +106,7 @@
    9.13        val wrappers =
    9.14          (Library.merge (eq_snd (op =)) (ws1, ws2), Library.merge (eq_snd (op =)) (ws1', ws2'));
    9.15        val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
    9.16 -          k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
    9.17 +          k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
    9.18        val next = ~ (length rules);
    9.19        val netpairs = fold (fn (n, (w, ((i, b), th))) =>
    9.20            nth_map i (curry insert_tagged_brl ((w, n), (b, th))))

    10.1 --- a/src/Pure/Isar/find_theorems.ML	Mon Feb 26 21:34:16 2007 +0100
    10.2 +++ b/src/Pure/Isar/find_theorems.ML	Mon Feb 26 23:18:24 2007 +0100
    10.3 @@ -227,7 +227,7 @@
    10.4    in
    10.5      map (`(eval_filters filters)) thms
    10.6      |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
    10.7 -    |> sort thm_ord |> map #2 
    10.8 +    |> sort thm_ord |> map #2
    10.9    end;
   10.10  
   10.11  end;
   10.12 @@ -236,32 +236,30 @@
   10.13  (* removing duplicates, preferring nicer names *)
   10.14  
   10.15  fun rem_thm_dups xs =
   10.16 -    let 
   10.17 -      fun nicer (Fact x) (Fact y) = size x <= size y
   10.18 -        | nicer (Fact _) _        = true
   10.19 -        | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
   10.20 -        | nicer (PureThy.Name _) (Fact _) = false
   10.21 -        | nicer (PureThy.Name _) _ = true
   10.22 -        | nicer (NameSelection (x,_)) (NameSelection (y,_)) = size x <= size y
   10.23 -        | nicer (NameSelection _) _ = false;
   10.24 +  let
   10.25 +    fun nicer (Fact x) (Fact y) = size x <= size y
   10.26 +      | nicer (Fact _) _        = true
   10.27 +      | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
   10.28 +      | nicer (PureThy.Name _) (Fact _) = false
   10.29 +      | nicer (PureThy.Name _) _ = true
   10.30 +      | nicer (NameSelection (x, _)) (NameSelection (y, _)) = size x <= size y
   10.31 +      | nicer (NameSelection _) _ = false;
   10.32  
   10.33 -      fun is_in [] _ = NONE
   10.34 -        | is_in ((n,t) :: xs) t' = if eq_thm (t, t') 
   10.35 -                                   then SOME (n,t) 
   10.36 -                                   else is_in xs t';
   10.37 +    fun is_in [] _ = NONE
   10.38 +      | is_in ((n, t) :: xs) t' =
   10.39 +          if Thm.eq_thm (t, t') then SOME (n, t) else is_in xs t';
   10.40  
   10.41 -      fun eq ((_,t1),(_,t2)) = eq_thm (t1,t2)
   10.42 +    fun eq ((_, t1), (_, t2)) = Thm.eq_thm (t1, t2);
   10.43  
   10.44 -      fun rem_d (rev_seen, []) = rev rev_seen
   10.45 -        | rem_d (rev_seen, (x as (n',t')) :: xs) = 
   10.46 -          case is_in rev_seen t' of 
   10.47 -            NONE => rem_d (x::rev_seen, xs)
   10.48 -          | SOME (n,t) => if nicer n n' 
   10.49 -                          then rem_d (rev_seen, xs) 
   10.50 -                          else rem_d (x::remove eq (n,t) rev_seen,xs)
   10.51 -
   10.52 -    in rem_d ([], xs) end;
   10.53 -
   10.54 +    fun rem_d (rev_seen, []) = rev rev_seen
   10.55 +      | rem_d (rev_seen, (x as (n', t')) :: xs) =
   10.56 +          (case is_in rev_seen t' of
   10.57 +            NONE => rem_d (x :: rev_seen, xs)
   10.58 +          | SOME (n, t) =>
   10.59 +              if nicer n n'
   10.60 +              then rem_d (rev_seen, xs)
   10.61 +              else rem_d (x :: remove eq (n, t) rev_seen, xs))
   10.62 +  in rem_d ([], xs) end;
   10.63  
   10.64  
   10.65  (* print_theorems *)
   10.66 @@ -272,7 +270,7 @@
   10.67    (ProofContext.lthms_containing ctxt spec
   10.68      |> maps PureThy.selections
   10.69      |> distinct (fn ((r1, th1), (r2, th2)) =>
   10.70 -        r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
   10.71 +        r1 = r2 andalso Thm.eq_thm_prop (th1, th2)));
   10.72  
   10.73  fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   10.74    let
   10.75 @@ -280,9 +278,10 @@
   10.76      val filters = map (filter_criterion ctxt opt_goal) criteria;
   10.77  
   10.78      val raw_matches = all_filters filters (find_thms ctxt ([], []));
   10.79 -    val matches = if rem_dups andalso not (null filters) 
   10.80 -                  then rem_thm_dups raw_matches 
   10.81 -                  else raw_matches;
   10.82 +    val matches =
   10.83 +      if rem_dups andalso not (null filters)
   10.84 +      then rem_thm_dups raw_matches
   10.85 +      else raw_matches;
   10.86  
   10.87      val len = length matches;
   10.88      val limit = the_default (! thms_containing_limit) opt_limit;

    11.1 --- a/src/Pure/Isar/induct_attrib.ML	Mon Feb 26 21:34:16 2007 +0100
    11.2 +++ b/src/Pure/Isar/induct_attrib.ML	Mon Feb 26 23:18:24 2007 +0100
    11.3 @@ -83,7 +83,7 @@
    11.4  
    11.5  val init_rules =
    11.6    NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
    11.7 -    Drule.eq_thm_prop (th1, th2));
    11.8 +    Thm.eq_thm_prop (th1, th2));
    11.9  
   11.10  fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
   11.11  

    12.1 --- a/src/Pure/Isar/net_rules.ML	Mon Feb 26 21:34:16 2007 +0100
    12.2 +++ b/src/Pure/Isar/net_rules.ML	Mon Feb 26 23:18:24 2007 +0100
    12.3 @@ -63,8 +63,8 @@
    12.4  
    12.5  (* intro/elim rules *)
    12.6  
    12.7 -val intro = init Drule.eq_thm_prop Thm.concl_of;
    12.8 -val elim = init Drule.eq_thm_prop Thm.major_prem_of;
    12.9 +val intro = init Thm.eq_thm_prop Thm.concl_of;
   12.10 +val elim = init Thm.eq_thm_prop Thm.major_prem_of;
   12.11  
   12.12  
   12.13  end;

    13.1 --- a/src/Pure/Proof/extraction.ML	Mon Feb 26 21:34:16 2007 +0100
    13.2 +++ b/src/Pure/Proof/extraction.ML	Mon Feb 26 23:18:24 2007 +0100
    13.3 @@ -206,7 +206,7 @@
    13.4       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
    13.5       types = merge_alists types1 types2,
    13.6       realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
    13.7 -     defs = gen_merge_lists eq_thm defs1 defs2,
    13.8 +     defs = gen_merge_lists Thm.eq_thm defs1 defs2,
    13.9       expand = merge_lists expand1 expand2,
   13.10       prep = (case prep1 of NONE => prep2 | _ => prep1)};
   13.11  
   13.12 @@ -373,7 +373,7 @@
   13.13           typeof_eqns = add_rule (([],
   13.14             Logic.dest_equals (prop_of (Drule.abs_def thm))), typeof_eqns),
   13.15           types = types,
   13.16 -         realizers = realizers, defs = insert eq_thm thm defs,
   13.17 +         realizers = realizers, defs = insert Thm.eq_thm thm defs,
   13.18           expand = expand, prep = prep}
   13.19        else
   13.20          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,

    14.1 --- a/src/Pure/Tools/codegen_data.ML	Mon Feb 26 21:34:16 2007 +0100
    14.2 +++ b/src/Pure/Tools/codegen_data.ML	Mon Feb 26 23:18:24 2007 +0100
    14.3 @@ -92,7 +92,7 @@
    14.4    then (false, xs)
    14.5    else (true, AList.merge eq_key eq xys);
    14.6  
    14.7 -val merge_thms = merge' eq_thm;
    14.8 +val merge_thms = merge' Thm.eq_thm;
    14.9  
   14.10  fun merge_lthms (r1, r2) =
   14.11    if Susp.same (r1, r2)
   14.12 @@ -123,7 +123,7 @@
   14.13      fun drop thm' = not (matches args (args_of thm'))
   14.14        orelse (warning ("Dropping redundant defining equation\n" ^ string_of_thm thm'); false);
   14.15      val (keeps, drops) = List.partition drop sels;
   14.16 -  in (thm :: keeps, dels |> fold (insert eq_thm) drops |> remove eq_thm thm) end;
   14.17 +  in (thm :: keeps, dels |> fold (insert Thm.eq_thm) drops |> remove Thm.eq_thm thm) end;
   14.18  
   14.19  fun add_thm thm (sels, dels) =
   14.20    apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
   14.21 @@ -136,7 +136,7 @@
   14.22        fold add_thm (Susp.force lthms) (sels, dels);
   14.23  
   14.24  fun del_thm thm (sels, dels) =
   14.25 -  (Susp.value (remove eq_thm thm (Susp.force sels)), thm :: dels);
   14.26 +  (Susp.value (remove Thm.eq_thm thm (Susp.force sels)), thm :: dels);
   14.27  
   14.28  fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
   14.29  
   14.30 @@ -145,8 +145,8 @@
   14.31      val (dels_t, dels) = merge_thms (dels1, dels2);
   14.32    in if dels_t
   14.33      then let
   14.34 -      val (_, sels) = merge_thms (Susp.force sels1, subtract eq_thm dels1 (Susp.force sels2))
   14.35 -      val (_, dels) = merge_thms (dels1, subtract eq_thm (Susp.force sels1) dels2)
   14.36 +      val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm dels1 (Susp.force sels2))
   14.37 +      val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm (Susp.force sels1) dels2)
   14.38      in (true, ((lazy o K) sels, dels)) end
   14.39      else let
   14.40        val (sels_t, sels) = merge_lthms (sels1, sels2)
   14.41 @@ -705,10 +705,10 @@
   14.42    in map_exec_purge (SOME consts) del thy end;
   14.43  
   14.44  fun add_inline thm thy =
   14.45 -  (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert eq_thm) (CodegenFunc.mk_rew thm)) thy;
   14.46 +  (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
   14.47  
   14.48  fun del_inline thm thy =
   14.49 -  (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove eq_thm) (CodegenFunc.mk_rew thm)) thy ;
   14.50 +  (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy ;
   14.51  
   14.52  fun add_inline_proc (name, f) =
   14.53    (map_exec_purge NONE o map_preproc o apfst o apsnd) (AList.update (op =) (name, (serial (), f)));

    15.1 --- a/src/Pure/Tools/nbe.ML	Mon Feb 26 21:34:16 2007 +0100
    15.2 +++ b/src/Pure/Tools/nbe.ML	Mon Feb 26 23:18:24 2007 +0100
    15.3 @@ -35,7 +35,7 @@
    15.4    val extend = I;
    15.5  
    15.6    fun merge _ ((pres1,posts1), (pres2,posts2)) =
    15.7 -    (Library.merge eq_thm (pres1,pres2), Library.merge eq_thm (posts1,posts2))
    15.8 +    (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
    15.9  
   15.10    fun print _ _ = ()
   15.11  end);
   15.12 @@ -44,9 +44,9 @@
   15.13    let
   15.14      fun map_data f = Context.mapping (NBE_Rewrite.map f) I;
   15.15      fun attr_pre (thy, thm) =
   15.16 -      ((map_data o apfst) (insert eq_thm thm) thy, thm)
   15.17 +      ((map_data o apfst) (insert Thm.eq_thm thm) thy, thm)
   15.18      fun attr_post (thy, thm) = 
   15.19 -      ((map_data o apsnd) (insert eq_thm thm) thy, thm)
   15.20 +      ((map_data o apsnd) (insert Thm.eq_thm thm) thy, thm)
   15.21      val attr = Attrib.syntax (Scan.lift (Args.$$$ "pre" >> K attr_pre
   15.22        || Args.$$$ "post" >> K attr_post));
   15.23    in

    16.1 --- a/src/Pure/drule.ML	Mon Feb 26 21:34:16 2007 +0100
    16.2 +++ b/src/Pure/drule.ML	Mon Feb 26 23:18:24 2007 +0100
    16.3 @@ -59,9 +59,6 @@
    16.4    val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
    16.5    val read_instantiate: (string*string)list -> thm -> thm
    16.6    val cterm_instantiate: (cterm*cterm)list -> thm -> thm
    16.7 -  val eq_thm_thy: thm * thm -> bool
    16.8 -  val eq_thm_prop: thm * thm -> bool
    16.9 -  val equiv_thm: thm * thm -> bool
   16.10    val size_of_thm: thm -> int
   16.11    val reflexive_thm: thm
   16.12    val symmetric_thm: thm
   16.13 @@ -557,30 +554,21 @@
   16.14  
   16.15  (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
   16.16  fun tha COMP thb =
   16.17 -    case distinct eq_thm (compose(tha,1,thb)) of
   16.18 +    case distinct Thm.eq_thm (compose(tha,1,thb)) of
   16.19          [th] => th
   16.20        | _ =>   raise THM("COMP", 1, [tha,thb]);
   16.21  
   16.22  
   16.23  (** theorem equality **)
   16.24  
   16.25 -(*True if the two theorems have the same theory.*)
   16.26 -val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm;
   16.27 -
   16.28 -(*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
   16.29 -val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
   16.30 -
   16.31  (*Useful "distance" function for BEST_FIRST*)
   16.32  val size_of_thm = size_of_term o Thm.full_prop_of;
   16.33  
   16.34  (*maintain lists of theorems --- preserving canonical order*)
   16.35 -val del_rule = remove eq_thm_prop;
   16.36 +val del_rule = remove Thm.eq_thm_prop;
   16.37  fun add_rule th = cons th o del_rule th;
   16.38 -val merge_rules = Library.merge eq_thm_prop;
   16.39 +val merge_rules = Library.merge Thm.eq_thm_prop;
   16.40  
   16.41 -(*pattern equivalence*)
   16.42 -fun equiv_thm ths =
   16.43 -  Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
   16.44  
   16.45  
   16.46  (*** Meta-Rewriting Rules ***)

    17.1 --- a/src/Pure/meta_simplifier.ML	Mon Feb 26 21:34:16 2007 +0100
    17.2 +++ b/src/Pure/meta_simplifier.ML	Mon Feb 26 23:18:24 2007 +0100
    17.3 @@ -147,7 +147,7 @@
    17.4  *)
    17.5  
    17.6  fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
    17.7 -  Drule.eq_thm_prop (thm1, thm2);
    17.8 +  Thm.eq_thm_prop (thm1, thm2);
    17.9  
   17.10  
   17.11  (* congruences *)
   17.12 @@ -155,7 +155,7 @@
   17.13  type cong = {thm: thm, lhs: cterm};
   17.14  
   17.15  fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
   17.16 -  Drule.eq_thm_prop (thm1, thm2);
   17.17 +  Thm.eq_thm_prop (thm1, thm2);
   17.18  
   17.19  
   17.20  (* simplification sets, procedures, and solvers *)
   17.21 @@ -238,7 +238,7 @@
   17.22  fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
   17.23  
   17.24  fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
   17.25 -  s1 = s2 andalso eq_list eq_thm (ths1, ths2);
   17.26 +  s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
   17.27  fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
   17.28  
   17.29  fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
   17.30 @@ -789,7 +789,7 @@
   17.31        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
   17.32  
   17.33      val rules' = Net.merge eq_rrule (rules1, rules2);
   17.34 -    val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2;
   17.35 +    val prems' = gen_merge_lists Thm.eq_thm_prop prems1 prems2;
   17.36      val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
   17.37      val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
   17.38      val weak' = merge (op =) (weak1, weak2);

    18.1 --- a/src/Pure/old_goals.ML	Mon Feb 26 21:34:16 2007 +0100
    18.2 +++ b/src/Pure/old_goals.ML	Mon Feb 26 23:18:24 2007 +0100
    18.3 @@ -392,9 +392,9 @@
    18.4    (case  Seq.pull(tac th)  of
    18.5       NONE      => error"by: tactic failed"
    18.6     | SOME(th2,ths2) =>
    18.7 -       (if eq_thm(th,th2)
    18.8 +       (if Thm.eq_thm(th,th2)
    18.9            then warning "Warning: same as previous level"
   18.10 -          else if eq_thm_thy(th,th2) then ()
   18.11 +          else if Thm.eq_thm_thy(th,th2) then ()
   18.12            else warning ("Warning: theory of proof state has changed" ^
   18.13                         thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
   18.14         ((th2,ths2)::(th,ths)::pairs)));
   18.15 @@ -414,9 +414,9 @@
   18.16       (case Seq.pull thstr of
   18.17            NONE      => (writeln"Going back a level..."; backtrack pairs)
   18.18          | SOME(th2,thstr2) =>
   18.19 -           (if eq_thm(th,th2)
   18.20 +           (if Thm.eq_thm(th,th2)
   18.21                then warning "Warning: same as previous choice at this level"
   18.22 -              else if eq_thm_thy(th,th2) then ()
   18.23 +              else if Thm.eq_thm_thy(th,th2) then ()
   18.24                else warning "Warning: theory of proof state has changed";
   18.25              (th2,thstr2)::pairs));
   18.26  

    19.1 --- a/src/Pure/search.ML	Mon Feb 26 21:34:16 2007 +0100
    19.2 +++ b/src/Pure/search.ML	Mon Feb 26 23:18:24 2007 +0100
    19.3 @@ -64,7 +64,7 @@
    19.4  	  case Seq.pull q of
    19.5  	      NONE         => depth used qs
    19.6  	    | SOME(st,stq) => 
    19.7 -		if satp st andalso not (member eq_thm used st)
    19.8 +		if satp st andalso not (member Thm.eq_thm used st)
    19.9  		then SOME(st, Seq.make
   19.10  			         (fn()=> depth (st::used) (stq::qs)))
   19.11  		else depth used (tac st :: stq :: qs)
   19.12 @@ -211,7 +211,7 @@
   19.13  (*Check for and delete duplicate proof states*)
   19.14  fun deleteAllMin prf heap = 
   19.15        if ThmHeap.is_empty heap then heap
   19.16 -      else if eq_thm (prf, #2 (ThmHeap.min heap))
   19.17 +      else if Thm.eq_thm (prf, #2 (ThmHeap.min heap))
   19.18        then deleteAllMin prf (ThmHeap.delete_min heap)
   19.19        else heap;
   19.20  
   19.21 @@ -269,7 +269,7 @@
   19.22  fun insert_with_level (lnth: int*int*thm, []) = [lnth]
   19.23    | insert_with_level ((l,m,th), (l',n,th')::nths) = 
   19.24        if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
   19.25 -      else if  n=m andalso eq_thm(th,th')
   19.26 +      else if  n=m andalso Thm.eq_thm(th,th')
   19.27                then (l',n,th')::nths
   19.28                else (l,m,th)::(l',n,th')::nths;
   19.29  

    20.1 --- a/src/Pure/tactic.ML	Mon Feb 26 21:34:16 2007 +0100
    20.2 +++ b/src/Pure/tactic.ML	Mon Feb 26 23:18:24 2007 +0100
    20.3 @@ -421,7 +421,7 @@
    20.4      foldr insert_tagged_brl netpair (taglist 1 brls);
    20.5  
    20.6  (*delete one kbrl from the pair of nets*)
    20.7 -fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
    20.8 +fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
    20.9  
   20.10  fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
   20.11    (if eres then

    21.1 --- a/src/Pure/tctical.ML	Mon Feb 26 21:34:16 2007 +0100
    21.2 +++ b/src/Pure/tctical.ML	Mon Feb 26 23:18:24 2007 +0100
    21.3 @@ -160,7 +160,7 @@
    21.4      | evyBack ((st',q,tacs)::trail) =
    21.5            case Seq.pull q of
    21.6                NONE        => evyBack trail
    21.7 -            | SOME(st,q') => if eq_thm (st',st)
    21.8 +            | SOME(st,q') => if Thm.eq_thm (st',st)
    21.9                               then evyBack ((st',q',tacs)::trail)
   21.10                               else EVY ((st,q',tacs)::trail, tacs) st
   21.11  in
   21.12 @@ -302,7 +302,7 @@
   21.13  (*Accept only next states that change the theorem's prop field
   21.14    (changes to signature, hyps, etc. don't count)*)
   21.15  fun CHANGED_PROP tac st =
   21.16 -  let fun diff st' = not (Drule.eq_thm_prop (st, st'));
   21.17 +  let fun diff st' = not (Thm.eq_thm_prop (st, st'));
   21.18    in Seq.filter diff (tac st) end;
   21.19  
   21.20  

    22.1 --- a/src/Sequents/prover.ML	Mon Feb 26 21:34:16 2007 +0100
    22.2 +++ b/src/Sequents/prover.ML	Mon Feb 26 23:18:24 2007 +0100
    22.3 @@ -32,15 +32,15 @@
    22.4         dups);
    22.5  
    22.6  fun (Pack(safes,unsafes)) add_safes ths   = 
    22.7 -    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
    22.8 -	val ths' = subtract Drule.eq_thm_prop dups ths
    22.9 +    let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes))
   22.10 +	val ths' = subtract Thm.eq_thm_prop dups ths
   22.11      in
   22.12          Pack(sort (make_ord less) (ths'@safes), unsafes)
   22.13      end;
   22.14  
   22.15  fun (Pack(safes,unsafes)) add_unsafes ths = 
   22.16 -    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
   22.17 -	val ths' = subtract Drule.eq_thm_prop dups ths
   22.18 +    let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,unsafes))
   22.19 +	val ths' = subtract Thm.eq_thm_prop dups ths
   22.20      in
   22.21  	Pack(safes, sort (make_ord less) (ths'@unsafes))
   22.22      end;

    23.1 --- a/src/ZF/Tools/typechk.ML	Mon Feb 26 21:34:16 2007 +0100
    23.2 +++ b/src/ZF/Tools/typechk.ML	Mon Feb 26 23:18:24 2007 +0100
    23.3 @@ -27,16 +27,16 @@
    23.4    net: thm Net.net};   (*discrimination net of the same rules*)
    23.5  
    23.6  fun add_rule th (tcs as TC {rules, net}) =
    23.7 -  if member Drule.eq_thm_prop rules th then
    23.8 +  if member Thm.eq_thm_prop rules th then
    23.9      (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
   23.10    else
   23.11      TC {rules = th :: rules,
   23.12          net = Net.insert_term (K false) (Thm.concl_of th, th) net};
   23.13  
   23.14  fun del_rule th (tcs as TC {rules, net}) =
   23.15 -  if member Drule.eq_thm_prop rules th then
   23.16 -    TC {net = Net.delete_term Drule.eq_thm_prop (Thm.concl_of th, th) net,
   23.17 -        rules = remove Drule.eq_thm_prop th rules}
   23.18 +  if member Thm.eq_thm_prop rules th then
   23.19 +    TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
   23.20 +        rules = remove Thm.eq_thm_prop th rules}
   23.21    else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
   23.22  
   23.23  
   23.24 @@ -51,7 +51,7 @@
   23.25  
   23.26    fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
   23.27      TC {rules = Drule.merge_rules (rules, rules'),
   23.28 -        net = Net.merge Drule.eq_thm_prop (net, net')};
   23.29 +        net = Net.merge Thm.eq_thm_prop (net, net')};
   23.30  
   23.31    fun print context (TC {rules, ...}) =
   23.32      Pretty.writeln (Pretty.big_list "type-checking rules:"