renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
authorwenzelm
Sun Jul 29 14:29:54 2007 +0200 (2007-07-29 ago)
changeset 24039273698405054
parent 24038 18182c4aec9e
child 24040 0d5cf52ebf87
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
src/HOL/Hyperreal/transfer.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/recdef_package.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/object_logic.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Sun Jul 29 14:29:52 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Sun Jul 29 14:29:54 2007 +0200
     1.3 @@ -30,14 +30,12 @@
     1.4        refolds = refolds1, consts = consts1},
     1.5       {intros = intros2, unfolds = unfolds2,
     1.6        refolds = refolds2, consts = consts2}) =
     1.7 -   {intros = Drule.merge_rules (intros1, intros2),
     1.8 -    unfolds = Drule.merge_rules (unfolds1, unfolds2),
     1.9 -    refolds = Drule.merge_rules (refolds1, refolds2),
    1.10 +   {intros = Thm.merge_thms (intros1, intros2),
    1.11 +    unfolds = Thm.merge_thms (unfolds1, unfolds2),
    1.12 +    refolds = Thm.merge_thms (refolds1, refolds2),
    1.13      consts = Library.merge (op =) (consts1, consts2)} : T;
    1.14  );
    1.15  
    1.16 -val transfer_start = thm "transfer_start"
    1.17 -
    1.18  fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
    1.19    | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
    1.20    | unstar_typ T = T
    1.21 @@ -48,7 +46,7 @@
    1.22            else (Const(a,unstar_typ T) $ unstar t)
    1.23        | unstar (f $ t) = unstar f $ unstar t
    1.24        | unstar (Const(a,T)) = Const(a,unstar_typ T)
    1.25 -      | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) 
    1.26 +      | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t)
    1.27        | unstar t = t
    1.28    in
    1.29      unstar term
    1.30 @@ -67,7 +65,7 @@
    1.31        rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
    1.32        ALLGOALS ObjectLogic.full_atomize_tac THEN
    1.33        match_tac [transitive_thm] 1 THEN
    1.34 -      resolve_tac [transfer_start] 1 THEN
    1.35 +      resolve_tac [@{thm transfer_start}] 1 THEN
    1.36        REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
    1.37        match_tac [reflexive_thm] 1
    1.38    in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
    1.39 @@ -92,14 +90,14 @@
    1.40    (fn {intros,unfolds,refolds,consts} =>
    1.41      {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
    1.42  in
    1.43 -val intro_add = Thm.declaration_attribute (map_intros o Drule.add_rule);
    1.44 -val intro_del = Thm.declaration_attribute (map_intros o Drule.del_rule);
    1.45 +val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm);
    1.46 +val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
    1.47  
    1.48 -val unfold_add = Thm.declaration_attribute (map_unfolds o Drule.add_rule);
    1.49 -val unfold_del = Thm.declaration_attribute (map_unfolds o Drule.del_rule);
    1.50 +val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm);
    1.51 +val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
    1.52  
    1.53 -val refold_add = Thm.declaration_attribute (map_refolds o Drule.add_rule);
    1.54 -val refold_del = Thm.declaration_attribute (map_refolds o Drule.del_rule);
    1.55 +val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm);
    1.56 +val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
    1.57  end
    1.58  
    1.59  fun add_const c = Context.theory_map (TransferData.map
     2.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Sun Jul 29 14:29:52 2007 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Jul 29 14:29:54 2007 +0200
     2.3 @@ -34,9 +34,9 @@
     2.4    type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
     2.5    val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
     2.6    val extend = I;
     2.7 -  fun merge _ (r1:T,r2:T) = {eqvts  = Drule.merge_rules (#eqvts r1, #eqvts r2),
     2.8 -                             freshs = Drule.merge_rules (#freshs r1, #freshs r2),
     2.9 -                             bijs   = Drule.merge_rules (#bijs r1, #bijs r2)}
    2.10 +  fun merge _ (r1:T,r2:T) = {eqvts  = Thm.merge_thms (#eqvts r1, #eqvts r2),
    2.11 +                             freshs = Thm.merge_thms (#freshs r1, #freshs r2),
    2.12 +                             bijs   = Thm.merge_thms (#bijs r1, #bijs r2)}
    2.13  );
    2.14  
    2.15  (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
    2.16 @@ -102,7 +102,7 @@
    2.17         val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
    2.18         val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
    2.19         val _ = Display.print_cterm (cterm_of thy goal_term)
    2.20 -   in	
    2.21 +   in
    2.22       Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
    2.23     end
    2.24  
    2.25 @@ -136,10 +136,10 @@
    2.26               (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
    2.27                 (Var (n,ty))) =>
    2.28               let
    2.29 -		(* FIXME: this should be an operation the library *)
    2.30 +                (* FIXME: this should be an operation the library *)
    2.31                  val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
    2.32 -	     in
    2.33 -		if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
    2.34 +             in
    2.35 +                if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
    2.36                  then [(pi,typi)]
    2.37                  else raise
    2.38                  EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
    2.39 @@ -177,7 +177,7 @@
    2.40         (* case: eqvt-lemma is of the equational form *)
    2.41        | (Const ("Trueprop", _) $ (Const ("op =", _) $
    2.42              (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
    2.43 -	   (if (apply_pi lhs (pi,typi)) = rhs
    2.44 +           (if (apply_pi lhs (pi,typi)) = rhs
    2.45                 then [orig_thm]
    2.46                 else raise EQVT_FORM "Type Equality")
    2.47        | _ => raise EQVT_FORM "Type unknown")
    2.48 @@ -205,15 +205,15 @@
    2.49  fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
    2.50  fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
    2.51  
    2.52 -val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
    2.53 -val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
    2.54 -val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
    2.55 -val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
    2.56 +val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Thm.add_thm));
    2.57 +val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Thm.del_thm));
    2.58 +val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Thm.add_thm));
    2.59 +val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Thm.del_thm));
    2.60  
    2.61 -val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
    2.62 -val bij_del   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
    2.63 -val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
    2.64 -val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
    2.65 +val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Thm.add_thm));
    2.66 +val bij_del   = Thm.declaration_attribute (bij_add_del_aux (bij_map Thm.del_thm));
    2.67 +val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Thm.add_thm));
    2.68 +val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Thm.del_thm));
    2.69  
    2.70  
    2.71  
    2.72 @@ -221,7 +221,7 @@
    2.73    Attrib.add_attributes
    2.74       [("eqvt",  Attrib.add_del_args eqvt_add eqvt_del,   "equivariance theorem declaration"),
    2.75        ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
    2.76 -                             "equivariance theorem declaration (without checking the form of the lemma)"),
    2.77 +        "equivariance theorem declaration (without checking the form of the lemma)"),
    2.78        ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
    2.79        ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")];
    2.80  
     3.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Sun Jul 29 14:29:52 2007 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Sun Jul 29 14:29:54 2007 +0200
     3.3 @@ -89,7 +89,7 @@
     3.4    type T = thm list
     3.5    val empty = []
     3.6    val extend = I
     3.7 -  fun merge _ = Drule.merge_rules
     3.8 +  fun merge _ = Thm.merge_thms
     3.9  );
    3.10  
    3.11  
    3.12 @@ -136,7 +136,7 @@
    3.13    type T = thm list
    3.14    val empty = []
    3.15    val extend = I
    3.16 -  fun merge _ = Drule.merge_rules
    3.17 +  fun merge _ = Thm.merge_thms
    3.18  );
    3.19  
    3.20  val get_termination_rules = TerminationRule.get
     4.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sun Jul 29 14:29:52 2007 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun Jul 29 14:29:54 2007 +0200
     4.3 @@ -172,14 +172,14 @@
     4.4  
     4.5  (* congruence rules *)
     4.6  
     4.7 -val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
     4.8 -val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
     4.9 +val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq);
    4.10 +val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq);
    4.11  
    4.12  (* Datatype hook to declare datatype congs as "fundef_congs" *)
    4.13  
    4.14  
    4.15  fun add_case_cong n thy =
    4.16 -    Context.theory_map (map_fundef_congs (Drule.add_rule
    4.17 +    Context.theory_map (map_fundef_congs (Thm.add_thm
    4.18                            (DatatypePackage.get_datatype thy n |> the
    4.19                             |> #case_cong
    4.20                             |> safe_mk_meta_eq)))
     5.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Jul 29 14:29:52 2007 +0200
     5.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Jul 29 14:29:54 2007 +0200
     5.3 @@ -134,7 +134,7 @@
     5.4    val empty = (Symtab.empty, []);
     5.5    val extend = I;
     5.6    fun merge _ ((tab1, monos1), (tab2, monos2)) =
     5.7 -    (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
     5.8 +    (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
     5.9  );
    5.10  
    5.11  val get_inductives = InductiveData.get o Context.Proof;
    5.12 @@ -187,8 +187,8 @@
    5.13      | _ => [thm]
    5.14    end handle THM _ => error ("Bad monotonicity theorem:\n" ^ string_of_thm thm);
    5.15  
    5.16 -val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono);
    5.17 -val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono);
    5.18 +val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
    5.19 +val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
    5.20  
    5.21  
    5.22  
     6.1 --- a/src/HOL/Tools/inductive_set_package.ML	Sun Jul 29 14:29:52 2007 +0200
     6.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Sun Jul 29 14:29:54 2007 +0200
     6.3 @@ -172,8 +172,8 @@
     6.4        set_arities = set_arities1, pred_arities = pred_arities1},
     6.5       {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
     6.6        set_arities = set_arities2, pred_arities = pred_arities2}) =
     6.7 -    {to_set_simps = Drule.merge_rules (to_set_simps1, to_set_simps2),
     6.8 -     to_pred_simps = Drule.merge_rules (to_pred_simps1, to_pred_simps2),
     6.9 +    {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
    6.10 +     to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
    6.11       set_arities = Symtab.merge_list op = (set_arities1, set_arities2),
    6.12       pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)};
    6.13  );
     7.1 --- a/src/HOL/Tools/recdef_package.ML	Sun Jul 29 14:29:52 2007 +0200
     7.2 +++ b/src/HOL/Tools/recdef_package.ML	Sun Jul 29 14:29:54 2007 +0200
     7.3 @@ -105,9 +105,9 @@
     7.4     ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
     7.5      (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
     7.6        (Symtab.merge (K true) (tab1, tab2),
     7.7 -        mk_hints (Drule.merge_rules (simps1, simps2),
     7.8 +        mk_hints (Thm.merge_thms (simps1, simps2),
     7.9            AList.merge (op =) Thm.eq_thm (congs1, congs2),
    7.10 -          Drule.merge_rules (wfs1, wfs2)));
    7.11 +          Thm.merge_thms (wfs1, wfs2)));
    7.12  );
    7.13  
    7.14  val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
    7.15 @@ -138,12 +138,12 @@
    7.16  
    7.17  fun attrib f = Thm.declaration_attribute (map_hints o f);
    7.18  
    7.19 -val simp_add = attrib (map_simps o Drule.add_rule);
    7.20 -val simp_del = attrib (map_simps o Drule.del_rule);
    7.21 +val simp_add = attrib (map_simps o Thm.add_thm);
    7.22 +val simp_del = attrib (map_simps o Thm.del_thm);
    7.23  val cong_add = attrib (map_congs o add_cong);
    7.24  val cong_del = attrib (map_congs o del_cong);
    7.25 -val wf_add = attrib (map_wfs o Drule.add_rule);
    7.26 -val wf_del = attrib (map_wfs o Drule.del_rule);
    7.27 +val wf_add = attrib (map_wfs o Thm.add_thm);
    7.28 +val wf_del = attrib (map_wfs o Thm.del_thm);
    7.29  
    7.30  
    7.31  (* modifiers *)
     8.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sun Jul 29 14:29:52 2007 +0200
     8.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Jul 29 14:29:54 2007 +0200
     8.3 @@ -122,11 +122,11 @@
     8.4        lessD = lessD1, neqE=neqE1, simpset = simpset1},
     8.5       {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
     8.6        lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
     8.7 -    {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
     8.8 -     mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2),
     8.9 -     inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
    8.10 -     lessD = Drule.merge_rules (lessD1, lessD2),
    8.11 -     neqE = Drule.merge_rules (neqE1, neqE2),
    8.12 +    {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2),
    8.13 +     mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2),
    8.14 +     inj_thms = Thm.merge_thms (inj_thms1, inj_thms2),
    8.15 +     lessD = Thm.merge_thms (lessD1, lessD2),
    8.16 +     neqE = Thm.merge_thms (neqE1, neqE2),
    8.17       simpset = Simplifier.merge_ss (simpset1, simpset2)};
    8.18  );
    8.19  
     9.1 --- a/src/Pure/Isar/calculation.ML	Sun Jul 29 14:29:52 2007 +0200
     9.2 +++ b/src/Pure/Isar/calculation.ML	Sun Jul 29 14:29:54 2007 +0200
     9.3 @@ -35,7 +35,7 @@
     9.4    val extend = I;
     9.5  
     9.6    fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
     9.7 -    ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
     9.8 +    ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
     9.9  );
    9.10  
    9.11  fun print_rules ctxt =
    9.12 @@ -71,10 +71,10 @@
    9.13  val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
    9.14  
    9.15  val sym_add =
    9.16 -  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule)
    9.17 +  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
    9.18    #> ContextRules.elim_query NONE;
    9.19  val sym_del =
    9.20 -  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule)
    9.21 +  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
    9.22    #> ContextRules.rule_del;
    9.23  
    9.24  
    10.1 --- a/src/Pure/Isar/local_defs.ML	Sun Jul 29 14:29:52 2007 +0200
    10.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Jul 29 14:29:54 2007 +0200
    10.3 @@ -151,15 +151,15 @@
    10.4    type T = thm list;
    10.5    val empty = []
    10.6    val extend = I;
    10.7 -  fun merge _ = Drule.merge_rules;
    10.8 +  fun merge _ = Thm.merge_thms;
    10.9  );
   10.10  
   10.11  fun print_rules ctxt =
   10.12    Pretty.writeln (Pretty.big_list "definitional transformations:"
   10.13      (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
   10.14  
   10.15 -val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
   10.16 -val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
   10.17 +val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
   10.18 +val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
   10.19  
   10.20  
   10.21  (* meta rewrite rules *)
    11.1 --- a/src/Pure/Isar/object_logic.ML	Sun Jul 29 14:29:52 2007 +0200
    11.2 +++ b/src/Pure/Isar/object_logic.ML	Sun Jul 29 14:29:54 2007 +0200
    11.3 @@ -51,7 +51,7 @@
    11.4  
    11.5    fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
    11.6      (merge_judgment (judgment1, judgment2),
    11.7 -      (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
    11.8 +      (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
    11.9  );
   11.10  
   11.11  
   11.12 @@ -141,8 +141,8 @@
   11.13  val get_atomize = #1 o #2 o ObjectLogicData.get;
   11.14  val get_rulify = #2 o #2 o ObjectLogicData.get;
   11.15  
   11.16 -val add_atomize = ObjectLogicData.map o apsnd o apfst o Drule.add_rule;
   11.17 -val add_rulify = ObjectLogicData.map o apsnd o apsnd o Drule.add_rule;
   11.18 +val add_atomize = ObjectLogicData.map o apsnd o apfst o Thm.add_thm;
   11.19 +val add_rulify = ObjectLogicData.map o apsnd o apsnd o Thm.add_thm;
   11.20  
   11.21  val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
   11.22  val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
    12.1 --- a/src/ZF/Tools/typechk.ML	Sun Jul 29 14:29:52 2007 +0200
    12.2 +++ b/src/ZF/Tools/typechk.ML	Sun Jul 29 14:29:54 2007 +0200
    12.3 @@ -49,7 +49,7 @@
    12.4    val extend = I;
    12.5  
    12.6    fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
    12.7 -    TC {rules = Drule.merge_rules (rules, rules'),
    12.8 +    TC {rules = Thm.merge_thms (rules, rules'),
    12.9          net = Net.merge Thm.eq_thm_prop (net, net')};
   12.10  );
   12.11