Sign.typ_instance;
authorwenzelm
Thu Jul 28 15:19:46 2005 +0200 (2005-07-28)
changeset 16931e41d8e319dfd
parent 16930 8d0daa50f381
child 16932 0bca871f5a21
Sign.typ_instance;
src/FOLP/simp.ML
     1.1 --- a/src/FOLP/simp.ML	Thu Jul 28 15:19:45 2005 +0200
     1.2 +++ b/src/FOLP/simp.ML	Thu Jul 28 15:19:46 2005 +0200
     1.3 @@ -544,20 +544,19 @@
     1.4      val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
     1.5  in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
     1.6  
     1.7 -fun find_subst tsig T =
     1.8 +fun find_subst sg T =
     1.9  let fun find (thm::thms) =
    1.10          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
    1.11              val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
    1.12              val eqT::_ = binder_types cT
    1.13 -        in if Type.typ_instance tsig (T,eqT) then SOME(thm,va,vb,P)
    1.14 +        in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
    1.15             else find thms
    1.16          end
    1.17        | find [] = NONE
    1.18  in find subst_thms end;
    1.19  
    1.20  fun mk_cong sg (f,aTs,rT) (refl,eq) =
    1.21 -let val tsig = Sign.tsig_of sg;
    1.22 -    val k = length aTs;
    1.23 +let val k = length aTs;
    1.24      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
    1.25          let val ca = cterm_of sg va
    1.26              and cx = cterm_of sg (eta_Var(("X"^si,0),T))
    1.27 @@ -568,7 +567,7 @@
    1.28          in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
    1.29      fun mk(c,T::Ts,i,yik) =
    1.30          let val si = radixstring(26,"a",i)
    1.31 -        in case find_subst tsig T of
    1.32 +        in case find_subst sg T of
    1.33               NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik)
    1.34             | SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik))
    1.35                         in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end
    1.36 @@ -578,10 +577,9 @@
    1.37  
    1.38  fun mk_cong_type sg (f,T) =
    1.39  let val (aTs,rT) = strip_type T;
    1.40 -    val tsig = Sign.tsig_of sg;
    1.41      fun find_refl(r::rs) =
    1.42          let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
    1.43 -        in if Type.typ_instance tsig (rT, hd(binder_types eqT))
    1.44 +        in if Sign.typ_instance sg (rT, hd(binder_types eqT))
    1.45             then SOME(r,(eq,body_type eqT)) else find_refl rs
    1.46          end
    1.47        | find_refl([]) = NONE;