removed thms_closure (unused);
authorwenzelm
Mon Sep 06 16:57:33 1999 +0200 (1999-09-06)
changeset 74861f9eceb434db
parent 7485 31a25b6af1b3
child 7487 c0f9b956a3e7
removed thms_closure (unused);
removed transfer_used_names;
fix: do not declare unconstrained vars;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 06 16:56:01 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 06 16:57:33 1999 +0200
     1.3 @@ -39,7 +39,6 @@
     1.4    val bind_propp_i: context * (term * (term list * term list)) -> context * term
     1.5    val auto_bind_goal: term -> context -> context
     1.6    val auto_bind_facts: string -> term list -> context -> context
     1.7 -  val thms_closure: context -> xstring -> thm list option
     1.8    val get_thm: context -> string -> thm
     1.9    val get_thms: context -> string -> thm list
    1.10    val get_thmss: context -> string list -> thm list
    1.11 @@ -58,7 +57,6 @@
    1.12      -> context -> context * ((string * thm list) list * thm list)
    1.13    val fix: (string list * string option) list -> context -> context
    1.14    val fix_i: (string list * typ) list -> context -> context
    1.15 -  val transfer_used_names: context -> context -> context
    1.16    val setup: (theory -> theory) list
    1.17  end;
    1.18  
    1.19 @@ -137,7 +135,8 @@
    1.20      fun pretty_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t));
    1.21    in
    1.22      if Vartab.is_empty binds andalso not (! verbose) then []
    1.23 -    else [Pretty.string_of (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds)))]
    1.24 +    else [Pretty.string_of (Pretty.big_list "Term bindings:"
    1.25 +      (map pretty_bind (Vartab.dest binds)))]
    1.26    end;
    1.27  
    1.28  val print_binds = seq writeln o strings_of_binds;
    1.29 @@ -585,18 +584,6 @@
    1.30  
    1.31  (** theorems **)
    1.32  
    1.33 -(* thms_closure *)
    1.34 -
    1.35 -fun thms_closure (Context {thy, thms, ...}) =
    1.36 -  let
    1.37 -    val global_closure = PureThy.thms_closure thy;
    1.38 -    fun get name =
    1.39 -      (case global_closure name of
    1.40 -        None => Symtab.lookup (thms, name)
    1.41 -      | some => some);
    1.42 -  in get end;
    1.43 -
    1.44 -
    1.45  (* get_thm(s) *)
    1.46  
    1.47  fun get_thm (ctxt as Context {thy, thms, ...}) name =
    1.48 @@ -687,30 +674,21 @@
    1.49  
    1.50  (* fix *)
    1.51  
    1.52 -fun read_skolemT (Context {defs = (_, _, _, used), ...}) None = Type.param used ("'z", logicS)
    1.53 -  | read_skolemT ctxt (Some s) = read_typ ctxt s;
    1.54 -
    1.55  fun gen_fix prep check (ctxt, (x, raw_T)) =
    1.56 -  ctxt
    1.57 -  |> declare_term (Free (check_skolem ctxt check x, prep ctxt raw_T))
    1.58 -  |> map_context (fn (thy, data, (assumes, (fixes, names)), binds, thms, defs) =>
    1.59 +  (check_skolem ctxt check x;
    1.60 +    ctxt
    1.61 +    |> (case prep ctxt raw_T of None => I | Some T => declare_term (Free (x, T)))
    1.62 +    |> map_context (fn (thy, data, (assumes, (fixes, names)), binds, thms, defs) =>
    1.63        let val x' = variant names x in
    1.64          (thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs)
    1.65 -      end);
    1.66 +      end));
    1.67  
    1.68  fun gen_fixs prep check vars ctxt =
    1.69    foldl (gen_fix prep check) (ctxt, flat (map (fn (xs, T) => map (rpair T) xs) vars));
    1.70  
    1.71 -
    1.72 -val fix = gen_fixs read_skolemT true;
    1.73 -val fix_i = gen_fixs cert_typ false;
    1.74 -
    1.75 +val fix = gen_fixs (apsome o read_typ) true;
    1.76 +val fix_i = gen_fixs (Some oo cert_typ) false;
    1.77  
    1.78 -(* used names *)
    1.79 -
    1.80 -fun transfer_used_names (Context {asms = (_, (_, names)), defs = (_, _, _, used), ...}) =
    1.81 -  map_context (fn (thy, data, (asms, (fixes, _)), binds, thms, (types, sorts, maxidx, _)) =>
    1.82 -    (thy, data, (asms, (fixes, names)), binds, thms, (types, sorts, maxidx, used)));
    1.83  
    1.84  
    1.85  (** theory setup **)