TFL/thry.ML
changeset 16935 4d7f19d340e8
parent 15798 016f3be5a5ec
child 17203 29b2563f5c11
equal deleted inserted replaced
16934:9ef19e3c7fdd 16935:4d7f19d340e8
    38     val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob)
    38     val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob)
    39     fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
    39     fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
    40   in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
    40   in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
    41   end;
    41   end;
    42 
    42 
    43 fun match_type thry pat ob = map tybind (Vartab.dest
    43 fun match_type thry pat ob =
    44   (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat, ob))));
    44   map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
    45 
    45 
    46 end;
    46 end;
    47 
    47 
    48 
    48 
    49 (*---------------------------------------------------------------------------
    49 (*---------------------------------------------------------------------------