removed obsolete TypeInfer.logicT -- use dummyT;
authorwenzelm
Sun Apr 15 23:25:50 2007 +0200 (2007-04-15)
changeset 227099ab51bac6287
parent 22708 fff918feff45
child 22710 f44439cdce77
removed obsolete TypeInfer.logicT -- use dummyT;
src/HOL/Import/proof_kernel.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/specification_package.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Syntax/mixfix.ML
src/Pure/sign.ML
src/Pure/simplifier.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Apr 15 23:25:49 2007 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Apr 15 23:25:50 2007 +0200
     1.3 @@ -473,10 +473,10 @@
     1.4  val check_name_thy = theory "Main"
     1.5  
     1.6  fun valid_boundvarname s =
     1.7 -  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
     1.8 +  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) ();
     1.9  
    1.10  fun valid_varname s =
    1.11 -  can (fn () => Thm.read_cterm check_name_thy (s, TypeInfer.logicT)) ();
    1.12 +  can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) ();
    1.13  
    1.14  fun protect_varname s =
    1.15      if innocent_varname s andalso valid_varname s then s else
     2.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 15 23:25:49 2007 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 15 23:25:50 2007 +0200
     2.3 @@ -388,8 +388,8 @@
     2.4      val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts
     2.5    in
     2.6      gen_primrec_i note def alt_name
     2.7 -      (Option.map (map (readt TypeInfer.logicT)) invs)
     2.8 -      (Option.map (readt TypeInfer.logicT) fctxt)
     2.9 +      (Option.map (map (readt dummyT)) invs)
    2.10 +      (Option.map (readt dummyT) fctxt)
    2.11        (names ~~ eqn_ts' ~~ atts) thy
    2.12    end;
    2.13  
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Apr 15 23:25:49 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Apr 15 23:25:50 2007 +0200
     3.3 @@ -157,7 +157,7 @@
     3.4      val (types, sorts) = types_sorts state;
     3.5      fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
     3.6        | types' ixn = types ixn;
     3.7 -    val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, TypeInfer.logicT)];
     3.8 +    val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, dummyT)];
     3.9    in case #T (rep_cterm ct) of
    3.10         Type (tn, _) => tn
    3.11       | _ => error ("Cannot determine type of " ^ quote aterm)
     4.1 --- a/src/HOL/Tools/specification_package.ML	Sun Apr 15 23:25:49 2007 +0200
     4.2 +++ b/src/HOL/Tools/specification_package.ML	Sun Apr 15 23:25:50 2007 +0200
     4.3 @@ -144,7 +144,7 @@
     4.4          val thawed_prop_consts = collect_consts (prop_thawed,[])
     4.5          val (altcos,overloaded) = Library.split_list cos
     4.6          val (names,sconsts) = Library.split_list altcos
     4.7 -        val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
     4.8 +        val consts = map (term_of o Thm.read_cterm thy o rpair dummyT) sconsts
     4.9          val _ = not (Library.exists (not o Term.is_Const) consts)
    4.10            orelse error "Specification: Non-constant found as parameter"
    4.11  
     5.1 --- a/src/Pure/Isar/find_theorems.ML	Sun Apr 15 23:25:49 2007 +0200
     5.2 +++ b/src/Pure/Isar/find_theorems.ML	Sun Apr 15 23:25:50 2007 +0200
     5.3 @@ -28,9 +28,9 @@
     5.4    | read_criterion _ Elim = Elim
     5.5    | read_criterion _ Dest = Dest
     5.6    | read_criterion ctxt (Simp str) =
     5.7 -      Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
     5.8 +      Simp (hd (ProofContext.read_term_pats dummyT ctxt [str]))
     5.9    | read_criterion ctxt (Pattern str) =
    5.10 -      Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
    5.11 +      Pattern (hd (ProofContext.read_term_pats dummyT ctxt [str]));
    5.12  
    5.13  fun pretty_criterion ctxt (b, c) =
    5.14    let
     6.1 --- a/src/Pure/Syntax/mixfix.ML	Sun Apr 15 23:25:49 2007 +0200
     6.2 +++ b/src/Pure/Syntax/mixfix.ML	Sun Apr 15 23:25:50 2007 +0200
     6.3 @@ -154,8 +154,8 @@
     6.4    | mixfix_args (Binder _) = 1
     6.5    | mixfix_args Structure = 0;
     6.6  
     6.7 -fun mixfixT (Binder _) = (TypeInfer.logicT --> TypeInfer.logicT) --> TypeInfer.logicT
     6.8 -  | mixfixT mx = replicate (mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;
     6.9 +fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
    6.10 +  | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
    6.11  
    6.12  
    6.13  (* syn_ext_types *)
     7.1 --- a/src/Pure/sign.ML	Sun Apr 15 23:25:49 2007 +0200
     7.2 +++ b/src/Pure/sign.ML	Sun Apr 15 23:25:50 2007 +0200
     7.3 @@ -610,7 +610,7 @@
     7.4  
     7.5      val args = sTs |> map (fn (s, raw_T) =>
     7.6        let val T = certify_typ thy raw_T handle TYPE (msg, _, _) => error msg
     7.7 -      in (read T s, T) end);
     7.8 +      in (read (#1 (TypeInfer.paramify_dummies T 0)) s, T) end);
     7.9  
    7.10      (*brute-force disambiguation via type-inference*)
    7.11      val termss = fold_rev (multiply o fst) args [[]];
    7.12 @@ -655,7 +655,7 @@
    7.13    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
    7.14    in t end handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
    7.15  
    7.16 -fun read_term thy = simple_read_term thy TypeInfer.logicT;
    7.17 +fun read_term thy = simple_read_term thy dummyT;
    7.18  fun read_prop thy = simple_read_term thy propT;
    7.19  
    7.20  
     8.1 --- a/src/Pure/simplifier.ML	Sun Apr 15 23:25:49 2007 +0200
     8.2 +++ b/src/Pure/simplifier.ML	Sun Apr 15 23:25:50 2007 +0200
     8.3 @@ -216,7 +216,7 @@
     8.4  (* FIXME *)
     8.5  fun read_terms ctxt ts =
     8.6    #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) []
     8.7 -    (map (rpair TypeInfer.logicT) ts));
     8.8 +    (map (rpair dummyT) ts));
     8.9  
    8.10  (* FIXME *)
    8.11  fun cert_terms ctxt ts = map (ProofContext.cert_term ctxt) ts;