fixed type signature of Type.varify
authorhaftmann
Tue Oct 31 09:29:06 2006 +0100 (2006-10-31 ago)
changeset 21116be58cded79da
parent 21115 f4e79a09c305
child 21117 e8657a20a52f
fixed type signature of Type.varify
src/HOL/Tools/old_inductive_package.ML
src/HOL/Tools/specification_package.ML
src/Pure/Proof/reconstruct.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/Tools/old_inductive_package.ML	Tue Oct 31 09:29:01 2006 +0100
     1.2 +++ b/src/HOL/Tools/old_inductive_package.ML	Tue Oct 31 09:29:06 2006 +0100
     1.3 @@ -173,14 +173,14 @@
     1.4    (let
     1.5      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     1.6      fun varify (t, (i, ts)) =
     1.7 -      let val t' = map_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
     1.8 +      let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
     1.9        in (maxidx_of_term t', t'::ts) end;
    1.10      val (i, cs') = foldr varify (~1, []) cs;
    1.11      val (i', intr_ts') = foldr varify (i, []) intr_ts;
    1.12      val rec_consts = fold add_term_consts_2 cs' [];
    1.13      val intr_consts = fold add_term_consts_2 intr_ts' [];
    1.14      fun unify (cname, cT) =
    1.15 -      let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
    1.16 +      let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
    1.17        in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
    1.18      val (env, _) = fold unify rec_consts (Vartab.empty, i');
    1.19      val subst = Type.freeze o map_types (Envir.norm_type env)
     2.1 --- a/src/HOL/Tools/specification_package.ML	Tue Oct 31 09:29:01 2006 +0100
     2.2 +++ b/src/HOL/Tools/specification_package.ML	Tue Oct 31 09:29:06 2006 +0100
     2.3 @@ -140,7 +140,7 @@
     2.4          val prop  = myfoldr HOLogic.mk_conj (map fst props'')
     2.5          val cprop = cterm_of thy (HOLogic.mk_Trueprop prop)
     2.6  
     2.7 -        val (prop_thawed,vmap) = Type.varify (prop,[])
     2.8 +        val (vmap, prop_thawed) = Type.varify [] prop
     2.9          val thawed_prop_consts = collect_consts (prop_thawed,[])
    2.10          val (altcos,overloaded) = Library.split_list cos
    2.11          val (names,sconsts) = Library.split_list altcos
    2.12 @@ -150,7 +150,7 @@
    2.13  
    2.14          fun proc_const c =
    2.15              let
    2.16 -                val c' = fst (Type.varify (c,[]))
    2.17 +                val (_, c') = Type.varify [] c
    2.18                  val (cname,ctyp) = dest_Const c'
    2.19              in
    2.20                  case List.filter (fn t => let val (name,typ) = dest_Const t
     3.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Oct 31 09:29:01 2006 +0100
     3.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Oct 31 09:29:06 2006 +0100
     3.3 @@ -144,7 +144,7 @@
     3.4            let
     3.5              val tvars = term_tvars prop;
     3.6              val tfrees = term_tfrees prop;
     3.7 -            val (prop', fmap) = Type.varify (prop, []);
     3.8 +            val (fmap, prop') = Type.varify [] prop;
     3.9              val (env', Ts) = (case opTs of
    3.10                  NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
    3.11                | SOME Ts => (env, Ts));
    3.12 @@ -306,7 +306,7 @@
    3.13    end;
    3.14  
    3.15  fun prop_of_atom prop Ts =
    3.16 -  let val (prop', fmap) = Type.varify (prop, []);
    3.17 +  let val (fmap, prop') = Type.varify [] prop;
    3.18    in subst_TVars (map fst (term_tvars prop) @ map snd fmap ~~ Ts)
    3.19      (forall_intr_vfs prop')
    3.20    end;
     4.1 --- a/src/Pure/thm.ML	Tue Oct 31 09:29:01 2006 +0100
     4.2 +++ b/src/Pure/thm.ML	Tue Oct 31 09:29:06 2006 +0100
     4.3 @@ -1176,7 +1176,7 @@
     4.4    let
     4.5      val tfrees = foldr add_term_tfrees fixed hyps;
     4.6      val prop1 = attach_tpairs tpairs prop;
     4.7 -    val (prop2, al) = Type.varify (prop1, tfrees);
     4.8 +    val (al, prop2) = Type.varify tfrees prop1;
     4.9      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
    4.10    in
    4.11      (al, Thm {thy_ref = thy_ref,
     5.1 --- a/src/Pure/type.ML	Tue Oct 31 09:29:01 2006 +0100
     5.2 +++ b/src/Pure/type.ML	Tue Oct 31 09:29:06 2006 +0100
     5.3 @@ -40,7 +40,7 @@
     5.4    (*special treatment of type vars*)
     5.5    val strip_sorts: typ -> typ
     5.6    val no_tvars: typ -> typ
     5.7 -  val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
     5.8 +  val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
     5.9    val freeze_thaw_type: typ -> typ * (typ -> typ)
    5.10    val freeze_type: typ -> typ
    5.11    val freeze_thaw: term -> term * (term -> term)
    5.12 @@ -228,7 +228,7 @@
    5.13  
    5.14  (* varify *)
    5.15  
    5.16 -fun varify (t, fixed) =
    5.17 +fun varify fixed t =
    5.18    let
    5.19      val fs = Term.fold_types (Term.fold_atyps
    5.20        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    5.21 @@ -238,7 +238,7 @@
    5.22        (case AList.lookup (op =) fmap f of
    5.23          NONE => TFree f
    5.24        | SOME xi => TVar (xi, S));
    5.25 -  in (map_types (map_type_tfree thaw) t, fmap) end;
    5.26 +  in (fmap, map_types (map_type_tfree thaw) t) end;
    5.27  
    5.28  
    5.29  (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)