# HG changeset patch
# User wenzelm
# Date 1176672350 -7200
# Node ID 9ab51bac6287ea795814f481e83aec103a7e554f
# Parent  fff918feff45e0b935de015da2fb68a80bf0717a
removed obsolete TypeInfer.logicT -- use dummyT;

diff -r fff918feff45 -r 9ab51bac6287 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -473,10 +473,10 @@
 val check_name_thy = theory "Main"
 
 fun valid_boundvarname s =
-  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
+  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) ();
 
 fun valid_varname s =
-  can (fn () => Thm.read_cterm check_name_thy (s, TypeInfer.logicT)) ();
+  can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) ();
 
 fun protect_varname s =
     if innocent_varname s andalso valid_varname s then s else
diff -r fff918feff45 -r 9ab51bac6287 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -388,8 +388,8 @@
     val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts
   in
     gen_primrec_i note def alt_name
-      (Option.map (map (readt TypeInfer.logicT)) invs)
-      (Option.map (readt TypeInfer.logicT) fctxt)
+      (Option.map (map (readt dummyT)) invs)
+      (Option.map (readt dummyT) fctxt)
       (names ~~ eqn_ts' ~~ atts) thy
   end;
 
diff -r fff918feff45 -r 9ab51bac6287 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -157,7 +157,7 @@
     val (types, sorts) = types_sorts state;
     fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
       | types' ixn = types ixn;
-    val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, TypeInfer.logicT)];
+    val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, dummyT)];
   in case #T (rep_cterm ct) of
        Type (tn, _) => tn
      | _ => error ("Cannot determine type of " ^ quote aterm)
diff -r fff918feff45 -r 9ab51bac6287 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/HOL/Tools/specification_package.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -144,7 +144,7 @@
         val thawed_prop_consts = collect_consts (prop_thawed,[])
         val (altcos,overloaded) = Library.split_list cos
         val (names,sconsts) = Library.split_list altcos
-        val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
+        val consts = map (term_of o Thm.read_cterm thy o rpair dummyT) sconsts
         val _ = not (Library.exists (not o Term.is_Const) consts)
           orelse error "Specification: Non-constant found as parameter"
 
diff -r fff918feff45 -r 9ab51bac6287 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -28,9 +28,9 @@
   | read_criterion _ Elim = Elim
   | read_criterion _ Dest = Dest
   | read_criterion ctxt (Simp str) =
-      Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
+      Simp (hd (ProofContext.read_term_pats dummyT ctxt [str]))
   | read_criterion ctxt (Pattern str) =
-      Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
+      Pattern (hd (ProofContext.read_term_pats dummyT ctxt [str]));
 
 fun pretty_criterion ctxt (b, c) =
   let
diff -r fff918feff45 -r 9ab51bac6287 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -154,8 +154,8 @@
   | mixfix_args (Binder _) = 1
   | mixfix_args Structure = 0;
 
-fun mixfixT (Binder _) = (TypeInfer.logicT --> TypeInfer.logicT) --> TypeInfer.logicT
-  | mixfixT mx = replicate (mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;
+fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
+  | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
 
 
 (* syn_ext_types *)
diff -r fff918feff45 -r 9ab51bac6287 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/Pure/sign.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -610,7 +610,7 @@
 
     val args = sTs |> map (fn (s, raw_T) =>
       let val T = certify_typ thy raw_T handle TYPE (msg, _, _) => error msg
-      in (read T s, T) end);
+      in (read (#1 (TypeInfer.paramify_dummies T 0)) s, T) end);
 
     (*brute-force disambiguation via type-inference*)
     val termss = fold_rev (multiply o fst) args [[]];
@@ -655,7 +655,7 @@
   let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
   in t end handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
 
-fun read_term thy = simple_read_term thy TypeInfer.logicT;
+fun read_term thy = simple_read_term thy dummyT;
 fun read_prop thy = simple_read_term thy propT;
 
 
diff -r fff918feff45 -r 9ab51bac6287 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/Pure/simplifier.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -216,7 +216,7 @@
 (* FIXME *)
 fun read_terms ctxt ts =
   #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) []
-    (map (rpair TypeInfer.logicT) ts));
+    (map (rpair dummyT) ts));
 
 (* FIXME *)
 fun cert_terms ctxt ts = map (ProofContext.cert_term ctxt) ts;