renamed Type.(un)varifyT to Logic.(un)varifyT;
authorwenzelm
Wed Jun 07 02:01:28 2006 +0200 (2006-06-07)
changeset 19806f860b7a98445
parent 19805 854404b8f738
child 19807 79161b339691
renamed Type.(un)varifyT to Logic.(un)varifyT;
made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
src/HOL/Library/word_setup.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/Tools/inductive_realizer.ML
src/Pure/IsaPlanner/term_lib.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_theorems.ML
src/Pure/codegen.ML
src/Pure/defs.ML
src/Pure/display.ML
src/Pure/logic.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/Library/word_setup.ML	Wed Jun 07 02:01:27 2006 +0200
     1.2 +++ b/src/HOL/Library/word_setup.ML	Wed Jun 07 02:01:28 2006 +0200
     1.3 @@ -35,8 +35,8 @@
     1.4  		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
     1.5  		else NONE
     1.6  	      | g _ _ _ = NONE
     1.7 -  (*lcp**	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***)
     1.8 -	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
     1.9 +  (*lcp**	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***)
    1.10 +	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
    1.11  	in
    1.12  	  Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
    1.13            thy
     2.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Jun 07 02:01:27 2006 +0200
     2.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Jun 07 02:01:28 2006 +0200
     2.3 @@ -147,7 +147,7 @@
     2.4       (foldr (fn ((f, p), prf) =>
     2.5          (case head_of (strip_abs_body f) of
     2.6             Free (s, T) =>
     2.7 -             let val T' = Type.varifyT T
     2.8 +             let val T' = Logic.varifyT T
     2.9               in Abst (s, SOME T', Proofterm.prf_abstract_over
    2.10                 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    2.11               end
    2.12 @@ -164,8 +164,7 @@
    2.13  
    2.14  fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) =
    2.15    let
    2.16 -    val sg = sign_of thy;
    2.17 -    val cert = cterm_of sg;
    2.18 +    val cert = cterm_of thy;
    2.19      val rT = TFree ("'P", HOLogic.typeS);
    2.20      val rT' = TVar (("'P", 0), HOLogic.typeS);
    2.21  
    2.22 @@ -187,7 +186,7 @@
    2.23      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
    2.24      val r = Const (case_name, map fastype_of rs ---> T --> rT);
    2.25  
    2.26 -    val y = Var (("y", 0), Type.varifyT T);
    2.27 +    val y = Var (("y", 0), Logic.legacy_varifyT T);
    2.28      val y' = Free ("y", T);
    2.29  
    2.30      val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
    2.31 @@ -208,10 +207,10 @@
    2.32      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    2.33      val prf = forall_intr_prf (y, forall_intr_prf (P,
    2.34        foldr (fn ((p, r), prf) =>
    2.35 -        forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
    2.36 +        forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p),
    2.37            prf))) (Proofterm.proof_combP (prf_of thm',
    2.38              map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
    2.39 -    val r' = Logic.varify (Abs ("y", Type.varifyT T,
    2.40 +    val r' = Logic.legacy_varify (Abs ("y", Logic.legacy_varifyT T,
    2.41        list_abs (map dest_Free rs, list_comb (r,
    2.42          map Bound ((length rs - 1 downto 0) @ [length rs])))));
    2.43  
     3.1 --- a/src/HOL/Tools/function_package/termination.ML	Wed Jun 07 02:01:27 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/termination.ML	Wed Jun 07 02:01:28 2006 +0200
     3.3 @@ -31,7 +31,7 @@
     3.4  fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom =
     3.5      let
     3.6  	val domT = domain_type (fastype_of f)
     3.7 -	val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
     3.8 +	val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
     3.9  	val DT = type_of D
    3.10  	val idomT = HOLogic.dest_setT DT
    3.11  
     4.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Jun 07 02:01:27 2006 +0200
     4.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jun 07 02:01:28 2006 +0200
     4.3 @@ -60,9 +60,9 @@
     4.4      val params = map dest_Var ts;
     4.5      val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
     4.6      fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
     4.7 -      map (Type.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
     4.8 +      map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
     4.9          filter_out (equal Extraction.nullT) (map
    4.10 -          (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    4.11 +          (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    4.12              NoSyn);
    4.13    in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
    4.14      map constr_of_intr intrs)
     5.1 --- a/src/Pure/IsaPlanner/term_lib.ML	Wed Jun 07 02:01:27 2006 +0200
     5.2 +++ b/src/Pure/IsaPlanner/term_lib.ML	Wed Jun 07 02:01:28 2006 +0200
     5.3 @@ -661,15 +661,15 @@
     5.4    fun change_vars_to_frees (a$b) =
     5.5          (change_vars_to_frees a) $ (change_vars_to_frees b)
     5.6      | change_vars_to_frees (Abs(s,ty,t)) =
     5.7 -        (Abs(s,Type.varifyT ty,change_vars_to_frees t))
     5.8 -    | change_vars_to_frees (Var((s,i),ty)) = (Free(s,Type.unvarifyT ty))
     5.9 +        (Abs(s, Logic.legacy_varifyT ty,change_vars_to_frees t))
    5.10 +    | change_vars_to_frees (Var((s,i),ty)) = (Free(s, Logic.legacy_unvarifyT ty))
    5.11      | change_vars_to_frees l = l;
    5.12  
    5.13    fun change_frees_to_vars (a$b) =
    5.14          (change_frees_to_vars a) $ (change_frees_to_vars b)
    5.15      | change_frees_to_vars (Abs(s,ty,t)) =
    5.16 -        (Abs(s,Type.varifyT ty,change_frees_to_vars t))
    5.17 -    | change_frees_to_vars (Free(s,ty)) = (Var((s,0),Type.varifyT ty))
    5.18 +        (Abs(s, Logic.legacy_varifyT ty,change_frees_to_vars t))
    5.19 +    | change_frees_to_vars (Free(s,ty)) = (Var((s,0), Logic.legacy_varifyT ty))
    5.20      | change_frees_to_vars l = l;
    5.21  
    5.22  
     6.1 --- a/src/Pure/Tools/class_package.ML	Wed Jun 07 02:01:27 2006 +0200
     6.2 +++ b/src/Pure/Tools/class_package.ML	Wed Jun 07 02:01:28 2006 +0200
     6.3 @@ -499,7 +499,7 @@
     6.4        in
     6.5          thy
     6.6          |> Sign.add_const_constraint_i (c, NONE)
     6.7 -        |> pair (c, Type.unvarifyT ty)
     6.8 +        |> pair (c, Logic.legacy_unvarifyT ty)
     6.9        end;
    6.10      fun check_defs0 thy raw_defs c_req =
    6.11        let
    6.12 @@ -508,8 +508,8 @@
    6.13          val c_given = map get_c raw_defs;
    6.14          fun eq_c ((c1 : string, ty1), (c2, ty2)) =
    6.15            let
    6.16 -            val ty1' = Type.varifyT ty1;
    6.17 -            val ty2' = Type.varifyT ty2;
    6.18 +            val ty1' = Logic.legacy_varifyT ty1;
    6.19 +            val ty2' = Logic.legacy_varifyT ty2;
    6.20            in
    6.21              c1 = c2
    6.22              andalso Sign.typ_instance thy (ty1', ty2')
    6.23 @@ -649,8 +649,8 @@
    6.24  
    6.25  fun extract_lookup thy sortctxt raw_typ_def raw_typ_use =
    6.26    let
    6.27 -    val typ_def = Type.varifyT raw_typ_def;
    6.28 -    val typ_use = Type.varifyT raw_typ_use;
    6.29 +    val typ_def = Logic.legacy_varifyT raw_typ_def;
    6.30 +    val typ_use = Logic.legacy_varifyT raw_typ_use;
    6.31      val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
    6.32      fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
    6.33      fun mk_class_deriv thy subclasses superclass =
    6.34 @@ -682,14 +682,14 @@
    6.35  fun extract_classlookup thy (c, raw_typ_use) =
    6.36    let
    6.37      val raw_typ_def = Sign.the_const_constraint thy c;
    6.38 -    val typ_def = Type.varifyT raw_typ_def;
    6.39 +    val typ_def = Logic.legacy_varifyT raw_typ_def;
    6.40      fun reorder_sortctxt ctxt =
    6.41        case lookup_const_class thy c
    6.42         of NONE => ctxt
    6.43          | SOME class =>
    6.44              let
    6.45                val data = the_class_data thy class;
    6.46 -              val sign = (Type.varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c;
    6.47 +              val sign = (Logic.legacy_varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c;
    6.48                val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty;
    6.49                val v : string = case Vartab.lookup match_tab (#var data, 0)
    6.50                  of SOME (_, TVar ((v, _), _)) => v;
     7.1 --- a/src/Pure/Tools/codegen_package.ML	Wed Jun 07 02:01:27 2006 +0200
     7.2 +++ b/src/Pure/Tools/codegen_package.ML	Wed Jun 07 02:01:28 2006 +0200
     7.3 @@ -605,7 +605,7 @@
     7.4        |> fold_map (ensure_def_class thy tabs) clss
     7.5        |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i))))
     7.6  and mk_fun thy tabs (c, ty) trns =
     7.7 -  case CodegenTheorems.get_funs thy (c, Type.varifyT ty)
     7.8 +  case CodegenTheorems.get_funs thy (c, Logic.legacy_varifyT ty)  (* FIXME *)
     7.9     of SOME (ty, eq_thms) =>
    7.10          let
    7.11            val sortctxt = ClassPackage.extract_sortctxt thy ty;
    7.12 @@ -849,7 +849,7 @@
    7.13  
    7.14  fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
    7.15    let
    7.16 -    val ty_def = (op ---> o apfst tl o strip_type o Type.unvarifyT o Sign.the_const_type thy) c;
    7.17 +    val ty_def = (op ---> o apfst tl o strip_type o Logic.legacy_unvarifyT o Sign.the_const_type thy) c;
    7.18      val ty' = (op ---> o apfst tl o strip_type) ty;
    7.19      val idf = idf_of_const thy tabs (c, ty);
    7.20    in
     8.1 --- a/src/Pure/Tools/codegen_theorems.ML	Wed Jun 07 02:01:27 2006 +0200
     8.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Wed Jun 07 02:01:28 2006 +0200
     8.3 @@ -619,7 +619,7 @@
     8.4  
     8.5  fun preprocess_term thy raw_t =
     8.6    let
     8.7 -    val t = (Term.map_term_types Type.varifyT o Logic.varify) raw_t;
     8.8 +    val t = Logic.legacy_varify raw_t;
     8.9      val x = variant (add_term_names (t, [])) "a";
    8.10      val t_eq = Logic.mk_equals (Free (x, fastype_of t), t);
    8.11      (*fake definition*)
     9.1 --- a/src/Pure/codegen.ML	Wed Jun 07 02:01:27 2006 +0200
     9.2 +++ b/src/Pure/codegen.ML	Wed Jun 07 02:01:28 2006 +0200
     9.3 @@ -558,7 +558,7 @@
     9.4  (**** retrieve definition of constant ****)
     9.5  
     9.6  fun is_instance thy T1 T2 =
     9.7 -  Sign.typ_instance thy (T1, Type.varifyT T2);
     9.8 +  Sign.typ_instance thy (T1, Logic.legacy_varifyT T2);
     9.9  
    9.10  fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) =>
    9.11    s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
    10.1 --- a/src/Pure/defs.ML	Wed Jun 07 02:01:27 2006 +0200
    10.2 +++ b/src/Pure/defs.ML	Wed Jun 07 02:01:28 2006 +0200
    10.3 @@ -33,7 +33,7 @@
    10.4    let
    10.5      val prt_args =
    10.6        if null args then []
    10.7 -      else [Pretty.list "(" ")" (map (Pretty.typ pp o Type.freeze_type) args)];
    10.8 +      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)];
    10.9    in Pretty.block (Pretty.str c :: prt_args) end;
   10.10  
   10.11  fun plain_args args =
    11.1 --- a/src/Pure/display.ML	Wed Jun 07 02:01:27 2006 +0200
    11.2 +++ b/src/Pure/display.ML	Wed Jun 07 02:01:28 2006 +0200
    11.3 @@ -169,7 +169,7 @@
    11.4      fun prt_sort S = Sign.pretty_sort thy S;
    11.5      fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]);
    11.6      fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
    11.7 -    val prt_typ_no_tvars = prt_typ o Type.freeze_type;
    11.8 +    val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
    11.9      fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
   11.10      val prt_term_no_vars = prt_term o Logic.unvarify;
   11.11      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    12.1 --- a/src/Pure/logic.ML	Wed Jun 07 02:01:27 2006 +0200
    12.2 +++ b/src/Pure/logic.ML	Wed Jun 07 02:01:28 2006 +0200
    12.3 @@ -67,8 +67,14 @@
    12.4    val set_rename_prefix: string -> unit
    12.5    val list_rename_params: string list * term -> term
    12.6    val assum_pairs: int * term -> (term*term)list
    12.7 +  val varifyT: typ -> typ
    12.8 +  val unvarifyT: typ -> typ
    12.9    val varify: term -> term
   12.10    val unvarify: term -> term
   12.11 +  val legacy_varifyT: typ -> typ
   12.12 +  val legacy_unvarifyT: typ -> typ
   12.13 +  val legacy_varify: term -> term
   12.14 +  val legacy_unvarify: term -> term
   12.15    val get_goal: term -> int -> term
   12.16    val goal_params: term -> int -> term * term list
   12.17    val prems_of_goal: term -> int -> term list
   12.18 @@ -492,7 +498,7 @@
   12.19        all T $ Abs(c, T, list_rename_params (cs, t))
   12.20    | list_rename_params (cs, B) = B;
   12.21  
   12.22 -(*** Treatmsent of "assume", "erule", etc. ***)
   12.23 +(*** Treatment of "assume", "erule", etc. ***)
   12.24  
   12.25  (*Strips assumptions in goal yielding
   12.26     HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   12.27 @@ -529,22 +535,46 @@
   12.28    in  pairrev (Hs,[])
   12.29    end;
   12.30  
   12.31 -(*Converts Frees to Vars and TFrees to TVars*)
   12.32 -fun varify (Const(a, T)) = Const (a, Type.varifyT T)
   12.33 -  | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
   12.34 -  | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
   12.35 -  | varify (t as Bound _) = t
   12.36 -  | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
   12.37 -  | varify (f $ t) = varify f $ varify t;
   12.38 +
   12.39 +(* global schematic variables *)
   12.40 +
   12.41 +fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
   12.42 +fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
   12.43 +
   12.44 +fun varifyT ty = ty |> Term.map_atyps
   12.45 +  (fn TFree (a, S) => TVar ((a, 0), S)
   12.46 +    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
   12.47 +
   12.48 +fun unvarifyT ty = ty |> Term.map_atyps
   12.49 +  (fn TVar ((a, 0), S) => TFree (a, S)
   12.50 +    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
   12.51 +    | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
   12.52  
   12.53 -(*Inverse of varify.*)
   12.54 -fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
   12.55 -  | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
   12.56 -  | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)
   12.57 -  | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T)  (*non-0 index!*)
   12.58 -  | unvarify (t as Bound _) = t
   12.59 -  | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body)
   12.60 -  | unvarify (f $ t) = unvarify f $ unvarify t;
   12.61 +fun varify tm =
   12.62 +  tm |> Term.map_aterms
   12.63 +    (fn Free (x, T) => Var ((x, 0), T)
   12.64 +      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   12.65 +      | t => t)
   12.66 +  |> Term.map_term_types varifyT;
   12.67 +
   12.68 +fun unvarify tm =
   12.69 +  tm |> Term.map_aterms
   12.70 +    (fn Var ((x, 0), T) => Free (x, T)
   12.71 +      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   12.72 +      | Free (x, _) => raise TERM (bad_fixed x, [tm])
   12.73 +      | t => t)
   12.74 +  |> Term.map_term_types unvarifyT;
   12.75 +
   12.76 +val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
   12.77 +val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
   12.78 +
   12.79 +val legacy_varify =
   12.80 +  Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
   12.81 +  Term.map_term_types legacy_varifyT;
   12.82 +
   12.83 +val legacy_unvarify =
   12.84 +  Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
   12.85 +  Term.map_term_types legacy_unvarifyT;
   12.86  
   12.87  
   12.88  (* goal states *)
    13.1 --- a/src/Pure/sign.ML	Wed Jun 07 02:01:27 2006 +0200
    13.2 +++ b/src/Pure/sign.ML	Wed Jun 07 02:01:28 2006 +0200
    13.3 @@ -721,7 +721,7 @@
    13.4  
    13.5  fun gen_add_consts prep_typ authentic raw_args thy =
    13.6    let
    13.7 -    val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
    13.8 +    val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
    13.9      fun prep (raw_c, raw_T, raw_mx) =
   13.10        let
   13.11          val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
   13.12 @@ -755,7 +755,7 @@
   13.13  
   13.14      val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
   13.15      val c' = Syntax.constN ^ full_name thy c;
   13.16 -    val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
   13.17 +    val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
   13.18        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   13.19      val T = Term.fastype_of t;
   13.20    in
   13.21 @@ -772,7 +772,7 @@
   13.22    let
   13.23      val c = int_const thy raw_c;
   13.24      fun prepT raw_T =
   13.25 -      let val T = Type.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T)))
   13.26 +      let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T)))
   13.27        in cert_term thy (Const (c, T)); T end
   13.28        handle TYPE (msg, _, _) => error msg;
   13.29    in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end;
    14.1 --- a/src/Pure/theory.ML	Wed Jun 07 02:01:27 2006 +0200
    14.2 +++ b/src/Pure/theory.ML	Wed Jun 07 02:01:28 2006 +0200
    14.3 @@ -240,7 +240,7 @@
    14.4      val consts = Sign.consts_of thy;
    14.5      fun prep const =
    14.6        let val Const (c, T) = Sign.no_vars pp (Const const)
    14.7 -      in (c, Consts.typargs consts (c, Compress.typ thy (Type.varifyT T))) end;
    14.8 +      in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end;
    14.9  
   14.10      val lhs_vars = Term.add_tfreesT (#2 lhs) [];
   14.11      val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
   14.12 @@ -267,7 +267,7 @@
   14.13        (case Sign.const_constraint thy c of
   14.14          NONE => error ("Undeclared constant " ^ quote c)
   14.15        | SOME declT => declT);
   14.16 -    val T' = Type.varifyT T;
   14.17 +    val T' = Logic.varifyT T;
   14.18  
   14.19      fun message txt =
   14.20        [Pretty.block [Pretty.str "Specification of constant ",
    15.1 --- a/src/Pure/type.ML	Wed Jun 07 02:01:27 2006 +0200
    15.2 +++ b/src/Pure/type.ML	Wed Jun 07 02:01:28 2006 +0200
    15.3 @@ -40,8 +40,6 @@
    15.4    (*special treatment of type vars*)
    15.5    val strip_sorts: typ -> typ
    15.6    val no_tvars: typ -> typ
    15.7 -  val varifyT: typ -> typ
    15.8 -  val unvarifyT: typ -> typ
    15.9    val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
   15.10    val freeze_thaw_type: typ -> typ * (typ -> typ)
   15.11    val freeze_type: typ -> typ
   15.12 @@ -228,10 +226,7 @@
   15.13        commas_quote (map (Term.string_of_vname o #1) vs), [T], []));
   15.14  
   15.15  
   15.16 -(* varify, unvarify *)
   15.17 -
   15.18 -val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
   15.19 -val unvarifyT = map_type_tvar (fn ((a, 0), S) => TFree (a, S) | v => TVar v);
   15.20 +(* varify *)
   15.21  
   15.22  fun varify (t, fixed) =
   15.23    let