Sign.infer_types: Name.context;
authorwenzelm
Wed Jul 19 12:12:06 2006 +0200 (2006-07-19)
changeset 2016308f2833ca433
parent 20162 d4bcb27686f9
child 20164 928c8dc07216
Sign.infer_types: Name.context;
FactIndex.add_local: simplified interface;
Variable.constraints_of;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jul 19 12:12:05 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jul 19 12:12:06 2006 +0200
     1.3 @@ -472,7 +472,7 @@
     1.4    let
     1.5      val types = append_env (Variable.def_type ctxt pattern) more_types;
     1.6      val sorts = append_env (Variable.def_sort ctxt) more_sorts;
     1.7 -    val used = Variable.used_types ctxt @ more_used;
     1.8 +    val used = fold Name.declare more_used (Variable.names_of ctxt);
     1.9    in
    1.10      (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) s
    1.11        handle TERM (msg, _) => error msg)
    1.12 @@ -534,14 +534,14 @@
    1.13  fun infer_type ctxt x =
    1.14    (case try (fn () =>
    1.15        Sign.infer_types (pp ctxt) (theory_of ctxt) (consts_of ctxt) (Variable.def_type ctxt false)
    1.16 -        (Variable.def_sort ctxt) (Variable.used_types ctxt) true
    1.17 +        (Variable.def_sort ctxt) (Variable.names_of ctxt) true
    1.18          ([Free (x, dummyT)], TypeInfer.logicT)) () of
    1.19      SOME (Free (_, T), _) => T
    1.20    | _ => error ("Failed to infer type of fixed variable " ^ quote x));
    1.21  
    1.22  fun inferred_param x ctxt =
    1.23    let val T = infer_type ctxt x
    1.24 -  in ((x, T), ctxt |> Variable.declare_syntax (Free (x, T))) end;
    1.25 +  in ((x, T), ctxt |> Variable.declare_term (Free (x, T))) end;
    1.26  
    1.27  fun inferred_fixes ctxt =
    1.28    fold_map inferred_param (rev (map #2 (Variable.fixes_of ctxt))) ctxt;
    1.29 @@ -550,7 +550,7 @@
    1.30  (* type and constant names *)
    1.31  
    1.32  fun read_tyname ctxt c =
    1.33 -  if member (op =) (Variable.used_types ctxt) c then
    1.34 +  if Syntax.is_tid c then
    1.35      TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (Variable.def_sort ctxt (c, ~1)))
    1.36    else Sign.read_tyname (theory_of ctxt) c;
    1.37  
    1.38 @@ -769,7 +769,7 @@
    1.39  fun put_thms _ ("", NONE) ctxt = ctxt
    1.40    | put_thms do_index ("", SOME ths) ctxt = ctxt |> map_thms (fn (facts, index) =>
    1.41        let
    1.42 -        val index' = FactIndex.add_local do_index (Variable.is_declared ctxt) ("", ths) index;
    1.43 +        val index' = FactIndex.add_local do_index ("", ths) index;
    1.44        in (facts, index') end)
    1.45    | put_thms _ (bname, NONE) ctxt = ctxt |> map_thms (fn ((space, tab), index) =>
    1.46        let
    1.47 @@ -781,7 +781,7 @@
    1.48          val name = full_name ctxt bname;
    1.49          val space' = NameSpace.declare (naming_of ctxt) name space;
    1.50          val tab' = Symtab.update (name, ths) tab;
    1.51 -        val index' = FactIndex.add_local do_index (Variable.is_declared ctxt) (name, ths) index;
    1.52 +        val index' = FactIndex.add_local do_index (name, ths) index;
    1.53        in ((space', tab'), index') end);
    1.54  
    1.55  fun put_thms_internal thms ctxt =
    1.56 @@ -819,7 +819,7 @@
    1.57  
    1.58  fun declare_var (x, opt_T, mx) ctxt =
    1.59    let val T = (case opt_T of SOME T => T | NONE => TypeInfer.mixfixT mx)
    1.60 -  in ((x, T, mx), ctxt |> Variable.declare_syntax (Free (x, T))) end;
    1.61 +  in ((x, T, mx), ctxt |> Variable.declare_constraints (Free (x, T))) end;
    1.62  
    1.63  local
    1.64  
    1.65 @@ -1060,7 +1060,7 @@
    1.66    let
    1.67      val (bind, ctxt') = bind_fixes [x] ctxt;
    1.68      val t = bind (Free (x, T));
    1.69 -  in (t, ctxt' |> Variable.declare_syntax t) end;
    1.70 +  in (t, ctxt' |> Variable.declare_constraints t) end;
    1.71  
    1.72  in
    1.73  
    1.74 @@ -1247,7 +1247,7 @@
    1.75      val prt_defT = prt_atom prt_var prt_typ;
    1.76      val prt_defS = prt_atom prt_varT prt_sort;
    1.77  
    1.78 -    val (types, sorts, used, _) = Variable.defaults_of ctxt;
    1.79 +    val (types, sorts) = Variable.constraints_of ctxt;
    1.80    in
    1.81      verb single (K pretty_thy) @
    1.82      pretty_ctxt ctxt @
    1.83 @@ -1256,8 +1256,7 @@
    1.84      verb pretty_lthms (K ctxt) @
    1.85      verb pretty_cases (K ctxt) @
    1.86      verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
    1.87 -    verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @
    1.88 -    verb single (fn () => Pretty.strs ("used type variable names:" :: rev used))
    1.89 +    verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
    1.90    end;
    1.91  
    1.92