--- a/TFL/tfl.ML Wed Jul 19 12:11:56 2006 +0200
+++ b/TFL/tfl.ML Wed Jul 19 12:11:57 2006 +0200
@@ -367,7 +367,7 @@
(*For Isabelle, the lhs of a definition must be a constant.*)
fun mk_const_def sign (c, Ty, rhs) =
- Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) [] false
+ Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) Name.context false
([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT)
|> #1;
--- a/src/HOLCF/domain/theorems.ML Wed Jul 19 12:11:56 2006 +0200
+++ b/src/HOLCF/domain/theorems.ML Wed Jul 19 12:11:57 2006 +0200
@@ -60,7 +60,7 @@
val pp = Sign.pp sg;
val consts = Sign.consts_of sg;
val (t, _) =
- Sign.infer_types pp sg consts (K NONE) (K NONE) [] true
+ Sign.infer_types pp sg consts (K NONE) (K NONE) Name.context true
([pre_tm],propT);
in t end;
--- a/src/HOLCF/fixrec_package.ML Wed Jul 19 12:11:56 2006 +0200
+++ b/src/HOLCF/fixrec_package.ML Wed Jul 19 12:11:57 2006 +0200
@@ -57,7 +57,7 @@
(* infers the type of a term *) (* FIXME better avoid this low-level stuff *)
(* similar to Theory.inferT_axm, but allows any type, not just propT *)
fun infer sg t =
- fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) [] true
+ fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) Name.context true
([t],dummyT));
(* builds the expression (LAM v. rhs) *)
--- a/src/Pure/Tools/nbe.ML Wed Jul 19 12:11:56 2006 +0200
+++ b/src/Pure/Tools/nbe.ML Wed Jul 19 12:11:57 2006 +0200
@@ -100,8 +100,7 @@
val vtab = var_tab t;
val ty = type_of t;
fun restrain ty t = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
- (K NONE) (K NONE)
- [] false ([t], ty) |> fst;
+ (K NONE) (K NONE) Name.context false ([t], ty) |> fst;
val _ = trace (fn () => "Normalized:\n" ^ NBE_Eval.string_of_nterm nt);
val t' = NBE_Codegen.nterm_to_term thy nt;
val _ = trace (fn () =>"Converted back:\n" ^ Display.raw_string_of_term t');
--- a/src/Pure/sign.ML Wed Jul 19 12:11:56 2006 +0200
+++ b/src/Pure/sign.ML Wed Jul 19 12:11:57 2006 +0200
@@ -177,14 +177,14 @@
val read_tyname: theory -> string -> typ
val read_const: theory -> string -> term
val infer_types_simult: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
- (indexname -> sort option) -> string list -> bool
+ (indexname -> sort option) -> Name.context -> bool
-> (term list * typ) list -> term list * (indexname * typ) list
val infer_types: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
- (indexname -> sort option) -> string list -> bool
+ (indexname -> sort option) -> Name.context -> bool
-> term list * typ -> term * (indexname * typ) list
val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
Context.generic -> (indexname -> typ option) * (indexname -> sort option) ->
- string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
+ Name.context -> bool -> (string * typ) list -> term list * (indexname * typ) list
val read_def_terms:
theory * (indexname -> typ option) * (indexname -> sort option) ->
string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
@@ -574,7 +574,7 @@
(*
def_type: partial map from indexnames to types (constrains Frees and Vars)
def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
- used: list of already used type variables
+ used: context of already used type variables
freeze: if true then generated parameters are turned into TFrees, else TVars
termss: lists of alternative parses (only one combination should be type-correct)
@@ -627,9 +627,9 @@
in (Syntax.read context is_logtype syn T' s, T') end;
in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
-fun read_def_terms (thy, types, sorts) =
+fun read_def_terms (thy, types, sorts) used =
read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (consts_of thy)
- (Context.Theory thy) (types, sorts);
+ (Context.Theory thy) (types, sorts) (Name.make_context used);
fun simple_read_term thy T s =
let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
--- a/src/Pure/theory.ML Wed Jul 19 12:11:56 2006 +0200
+++ b/src/Pure/theory.ML Wed Jul 19 12:11:57 2006 +0200
@@ -195,7 +195,8 @@
let
val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
val (t, _) =
- Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) types sorts used true (ts, propT);
+ Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
+ types sorts (Name.make_context used) true (ts, propT);
in cert_axm thy (name, t) end
handle ERROR msg => err_in_axm msg name;
@@ -205,7 +206,8 @@
let
val pp = Sign.pp thy;
val (t, _) =
- Sign.infer_types pp thy (Sign.consts_of thy) (K NONE) (K NONE) [] true ([pre_tm], propT);
+ Sign.infer_types pp thy (Sign.consts_of thy)
+ (K NONE) (K NONE) Name.context true ([pre_tm], propT);
in (name, Sign.no_vars pp t) end
handle ERROR msg => err_in_axm msg name;