adapted names of some sort ops;
authorwenzelm
Fri May 21 21:27:10 2004 +0200 (2004-05-21)
changeset 1479123e51b22c710
parent 14790 0d984ee030a1
child 14792 b7dac2fae5bb
adapted names of some sort ops;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Fri May 21 21:26:19 2004 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri May 21 21:27:10 2004 +0200
     1.3 @@ -328,7 +328,7 @@
     1.4        rep_thm th2;
     1.5    in
     1.6      Sign.joinable (sg1, sg2) andalso
     1.7 -    eq_set_sort (shyps1, shyps2) andalso
     1.8 +    Sorts.eq_set_sort (shyps1, shyps2) andalso
     1.9      aconvs (hyps1, hyps2) andalso
    1.10      aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso
    1.11      prop1 aconv prop2
    1.12 @@ -393,8 +393,8 @@
    1.13    to improve efficiency a bit*)
    1.14  
    1.15  fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
    1.16 -  | add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss)
    1.17 -  | add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss)
    1.18 +  | add_typ_sorts (TFree (_, S), Ss) = Sorts.ins_sort(S,Ss)
    1.19 +  | add_typ_sorts (TVar (_, S), Ss) = Sorts.ins_sort(S,Ss)
    1.20  and add_typs_sorts ([], Ss) = Ss
    1.21    | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));
    1.22  
    1.23 @@ -422,17 +422,17 @@
    1.24  
    1.25  fun add_thms_shyps ([], Ss) = Ss
    1.26    | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
    1.27 -      add_thms_shyps (ths, union_sort (shyps, Ss));
    1.28 +      add_thms_shyps (ths, Sorts.union_sort (shyps, Ss));
    1.29  
    1.30  
    1.31  (*get 'dangling' sort constraints of a thm*)
    1.32  fun extra_shyps (th as Thm {shyps, ...}) =
    1.33 -  Term.rems_sort (shyps, add_thm_sorts (th, []));
    1.34 +  Sorts.rems_sort (shyps, add_thm_sorts (th, []));
    1.35  
    1.36  
    1.37  (* fix_shyps *)
    1.38  
    1.39 -fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref));
    1.40 +fun all_sorts_nonempty sign_ref = is_some (Sign.universal_witness (Sign.deref sign_ref));
    1.41  
    1.42  (*preserve sort contexts of rule premises and substituted types*)
    1.43  fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, tpairs, prop, ...}) =
    1.44 @@ -455,11 +455,11 @@
    1.45          val sign = Sign.deref sign_ref;
    1.46  
    1.47          val present_sorts = add_thm_sorts (thm, []);
    1.48 -        val extra_shyps = Term.rems_sort (shyps, present_sorts);
    1.49 +        val extra_shyps = Sorts.rems_sort (shyps, present_sorts);
    1.50          val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps;
    1.51        in
    1.52          Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
    1.53 -             shyps = Term.rems_sort (shyps, map #2 witnessed_shyps),
    1.54 +             shyps = Sorts.rems_sort (shyps, map #2 witnessed_shyps),
    1.55               hyps = hyps, tpairs = tpairs, prop = prop}
    1.56        end;
    1.57  
    1.58 @@ -616,7 +616,7 @@
    1.59                    Thm{sign_ref= merge_thm_sgs(thAB,thA),
    1.60                        der = Pt.infer_derivs (curry Pt.%%) der derA,
    1.61                        maxidx = Int.max(maxA,maxidx),
    1.62 -                      shyps = union_sort (shypsA, shyps),
    1.63 +                      shyps = Sorts.union_sort (shypsA, shyps),
    1.64                        hyps = union_term(hypsA,hyps),  (*dups suppressed*)
    1.65                        tpairs = tpairsA @ tpairs,
    1.66                        prop = B}
    1.67 @@ -726,7 +726,7 @@
    1.68                   Thm{sign_ref= merge_thm_sgs(th1,th2), 
    1.69                       der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
    1.70                       maxidx = Int.max(max1,max2), 
    1.71 -                     shyps = union_sort (shyps1, shyps2),
    1.72 +                     shyps = Sorts.union_sort (shyps1, shyps2),
    1.73                       hyps = union_term(hyps1,hyps2),
    1.74                       tpairs = tpairs1 @ tpairs2,
    1.75                       prop = eq$t1$t2}
    1.76 @@ -824,7 +824,7 @@
    1.77                              der = Pt.infer_derivs
    1.78                                (Pt.combination f g t u fT) der1 der2,
    1.79                              maxidx = Int.max(max1,max2), 
    1.80 -                            shyps = union_sort(shyps1,shyps2),
    1.81 +                            shyps = Sorts.union_sort(shyps1,shyps2),
    1.82                              hyps = union_term(hyps1,hyps2),
    1.83                              tpairs = tpairs1 @ tpairs2,
    1.84                              prop = Logic.mk_equals(f$t, g$u)}
    1.85 @@ -855,7 +855,7 @@
    1.86                Thm{sign_ref = merge_thm_sgs(th1,th2),
    1.87                    der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
    1.88                    maxidx = Int.max(max1,max2),
    1.89 -                  shyps = union_sort(shyps1,shyps2),
    1.90 +                  shyps = Sorts.union_sort(shyps1,shyps2),
    1.91                    hyps = union_term(hyps1,hyps2),
    1.92                    tpairs = tpairs1 @ tpairs2,
    1.93                    prop = Logic.mk_equals(A,B)}
    1.94 @@ -973,7 +973,7 @@
    1.95    let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[]));
    1.96        val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[]));
    1.97        val tsig = Sign.tsig_of (Sign.deref newsign_ref);
    1.98 -      fun subst t = subst_atomic tpairs (Type.inst_term_tvars (tsig, vTs) t);
    1.99 +      fun subst t = subst_atomic tpairs (Type.inst_term_tvars tsig vTs t);
   1.100        val newprop = subst prop;
   1.101        val newdpairs = map (pairself subst) dpairs;
   1.102        val newth =
   1.103 @@ -1093,8 +1093,8 @@
   1.104        Thm{sign_ref = merge_thm_sgs(state,orule),
   1.105            der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der,
   1.106            maxidx = maxidx+smax+1,
   1.107 -          shyps=union_sort(sshyps,shyps), 
   1.108 -          hyps=hyps, 
   1.109 +          shyps = Sorts.union_sort(sshyps,shyps), 
   1.110 +          hyps = hyps, 
   1.111            tpairs = map (pairself lift_abs) tpairs,
   1.112            prop = Logic.list_implies (map lift_all As, lift_all B)}
   1.113    end;
   1.114 @@ -1371,7 +1371,7 @@
   1.115                         curry op oo (Pt.norm_proof' env))
   1.116                      (Pt.bicompose_proof Bs oldAs As A n)) rder' sder,
   1.117                   maxidx = maxidx,
   1.118 -                 shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
   1.119 +                 shyps = add_env_sorts (env, Sorts.union_sort(rshyps,sshyps)),
   1.120                   hyps = union_term(rhyps,shyps),
   1.121                   tpairs = ntpairs,
   1.122                   prop = Logic.list_implies normp}