src/HOL/Tools/record_package.ML
changeset 16934 9ef19e3c7fdd
parent 16872 a51699621d22
child 16973 b2a894562b8f
     1.1 --- a/src/HOL/Tools/record_package.ML	Thu Jul 28 15:19:48 2005 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Thu Jul 28 15:19:49 2005 +0200
     1.3 @@ -429,9 +429,7 @@
     1.4      val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name));
     1.5      val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname)))));
     1.6  
     1.7 -    val tsig = Sign.tsig_of sg;
     1.8 -    fun unify (t,env) = Type.unify tsig env t;
     1.9 -    val (subst,_) = foldr unify (Vartab.empty,0) (but_last args ~~ but_last Ts);
    1.10 +    val (subst,_) = fold (Sign.typ_unify sg) (but_last args ~~ but_last Ts) (Vartab.empty,0);
    1.11      val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
    1.12    in (flds',(more,moreT)) end;
    1.13  
    1.14 @@ -570,12 +568,10 @@
    1.15                                | NONE => Sign.defaultS sg);
    1.16      
    1.17   
    1.18 -    val tsig = Sign.tsig_of sg;
    1.19 -    fun to_type t = Type.cert_typ tsig 
    1.20 +    fun to_type t = Sign.certify_typ sg
    1.21                         (Sign.intern_typ sg 
    1.22                           (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t));
    1.23 -    fun unify (t,env) = Type.unify tsig env t; 
    1.24 -    
    1.25 +
    1.26      fun mk_ext (fargs as (name,arg)::_) =
    1.27           (case get_fieldext sg (Sign.intern_const sg name) of
    1.28              SOME (ext,alphas) => 
    1.29 @@ -587,9 +583,10 @@
    1.30                         val (args,rest) = splitargs (map fst flds') fargs;
    1.31                         val vartypes = map Type.varifyT types;
    1.32                         val argtypes = map to_type args;
    1.33 -                       val (subst,_) = foldr unify (Vartab.empty,0) (vartypes ~~ argtypes);
    1.34 +                       val (subst,_) = fold (Sign.typ_unify sg) (vartypes ~~ argtypes)
    1.35 +                                            (Vartab.empty,0);
    1.36                         val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o 
    1.37 -                                          (Envir.norm_type subst) o Type.varifyT) 
    1.38 +                                          Envir.norm_type subst o Type.varifyT) 
    1.39                                           (but_last alphas);
    1.40   
    1.41                         val more' = mk_ext rest;   
    1.42 @@ -727,13 +724,12 @@
    1.43        
    1.44        val T = fixT (Sign.intern_typ sg 
    1.45                        (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); 
    1.46 -      val tsig = Sign.tsig_of sg
    1.47  
    1.48        fun mk_type_abbr subst name alphas = 
    1.49            let val abbrT = Type (name, map (fn a => TVar ((a, 0), Sign.defaultS sg)) alphas);
    1.50            in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
    1.51  
    1.52 -      fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T));
    1.53 +      fun unify rT T = fst (Sign.typ_unify sg (Type.varifyT rT,T) (Vartab.empty,0));
    1.54  
    1.55     in if !print_record_type_abbr
    1.56        then (case last_extT T of
    1.57 @@ -760,9 +756,6 @@
    1.58  
    1.59      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
    1.60  
    1.61 -    val tsig = Sign.tsig_of sg
    1.62 -    fun unify (t,v) = Type.unify tsig v t;
    1.63 -
    1.64      fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T);
    1.65   
    1.66      fun field_lst T =
    1.67 @@ -780,8 +773,9 @@
    1.68                                              ::map (apfst NameSpace.base) fs; 
    1.69                                  val (args',more) = split_last args; 
    1.70                                  val alphavars = map Type.varifyT (but_last alphas); 
    1.71 -                                val (subst,_)= foldr unify (Vartab.empty,0) (alphavars~~args');
    1.72 -                                val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT)))
    1.73 +                                val (subst,_)= fold (Sign.typ_unify sg) (alphavars~~args')
    1.74 +                                                    (Vartab.empty,0);
    1.75 +                                val flds'' =map (apsnd (Envir.norm_type subst o Type.varifyT))
    1.76                                                  flds';
    1.77                                in flds''@field_lst more end
    1.78                                handle TUNIFY         => [("",T)]