# HG changeset patch
# User wenzelm
# Date 947069764 -3600
# Node ID 6186ee807f2ea3829a4b62944216b1448a3490b1
# Parent  6a087be9f6d9cde6fc270e523a924070f1ef6f54
replaced HOLogic.termTVar by HOLogic.termT;

diff -r 6a087be9f6d9 -r 6186ee807f2e src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/Arith.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -821,7 +821,7 @@
 
 (** prepare nat_cancel simprocs **)
 
-fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termTVar);
+fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT);
 val prep_pats = map prep_pat;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
diff -r 6a087be9f6d9 -r 6186ee807f2e src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/Prod.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -171,7 +171,7 @@
 	(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
 	(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
   fun simproc name patstr = Simplifier.mk_simproc name 
-		[Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termTVar)];
+		[Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termT)];
 
   val beta_patstr = "split f z";
   val  eta_patstr = "split f";
diff -r 6a087be9f6d9 -r 6186ee807f2e src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -150,8 +150,7 @@
     val (types, sorts) = types_sorts state;
     fun types' (a, ~1) = (case assoc (params, a) of None => types(a, ~1) | sm => sm)
       | types' ixn = types ixn;
-    val (ct, _) = read_def_cterm (sign, types', sorts) [] false
-                                  (aterm, TVar (("", 0), []));
+    val (ct, _) = read_def_cterm (sign, types', sorts) [] false (aterm, TypeInfer.logicT);
   in case #T (rep_cterm ct) of
        Type (tn, _) => tn
      | _ => error ("Cannot determine type of " ^ quote aterm)
@@ -248,7 +247,7 @@
    | _ => None)
   | distinct_proc sg _ _ = None;
 
-val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termTVar)];
+val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termT)];
 val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
 
 val dist_ss = HOL_ss addsimprocs [distinct_simproc];
diff -r 6a087be9f6d9 -r 6186ee807f2e src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -777,7 +777,7 @@
 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   let
     val sign = Theory.sign_of thy;
-    val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termTVar) c_strings;
+    val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
 
     val atts = map (Attrib.global_attribute thy) srcs;
     val intr_names = map (fst o fst) intro_srcs;
diff -r 6a087be9f6d9 -r 6186ee807f2e src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -466,7 +466,7 @@
 
 local
 
-val sel_upd_pat = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s (u k r)", HOLogic.termTVar)];
+val sel_upd_pat = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s (u k r)", HOLogic.termT)];
 
 fun proc sg _ t =
   (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
diff -r 6a087be9f6d9 -r 6186ee807f2e src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -89,7 +89,7 @@
 (* prepare_typedef *)
 
 fun read_term sg used s =
-  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termTVar));
+  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT));
 
 fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
 
diff -r 6a087be9f6d9 -r 6186ee807f2e src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/hologic.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -9,7 +9,7 @@
 sig
   val termC: class
   val termS: sort
-  val termTVar: typ
+  val termT: typ
   val boolT: typ
   val false_const: term
   val true_const: term
@@ -75,8 +75,7 @@
 
 val termC: class = "term";
 val termS: sort = [termC];
-
-val termTVar = TVar (("'a", 0), termS);
+val termT = TypeInfer.anyT termS;
 
 
 (* bool and set *)
diff -r 6a087be9f6d9 -r 6186ee807f2e src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -470,7 +470,7 @@
 (* external interfaces *)
 
 fun read_term sg str =
-  read_cterm sg (str, HOLogic.termTVar);
+  read_cterm sg (str, HOLogic.termT);
 
 fun cert_term sg tm =
   cterm_of sg tm handle TERM (msg, _) => error msg;