# HG changeset patch
# User wenzelm
# Date 1153303917 -7200
# Node ID da0505518e690bc456204fe19e2482936d46977f
# Parent  c709a29f1363846c3069c387ab0f3cd9608e7c4f
Sign.infer_types: Name.context;

diff -r c709a29f1363 -r da0505518e69 TFL/tfl.ML
--- 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;
 
diff -r c709a29f1363 -r da0505518e69 src/HOLCF/domain/theorems.ML
--- 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;
 
diff -r c709a29f1363 -r da0505518e69 src/HOLCF/fixrec_package.ML
--- 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) *)
diff -r c709a29f1363 -r da0505518e69 src/Pure/Tools/nbe.ML
--- 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');
diff -r c709a29f1363 -r da0505518e69 src/Pure/sign.ML
--- 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)]
diff -r c709a29f1363 -r da0505518e69 src/Pure/theory.ML
--- 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;