# HG changeset patch # User wenzelm # Date 1194548889 -3600 # Node ID 17f04d987f37034efd8a91b14d79e5ac87a2f39e # Parent 24d1568af397b21dc3dbc3358d8f5c07b95798d7 removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy; discontinued legacy_intern_skolem, gen_read'; diff -r 24d1568af397 -r 17f04d987f37 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Nov 08 20:08:07 2007 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Nov 08 20:08:09 2007 +0100 @@ -62,9 +62,6 @@ val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term val expand_abbrevs: Proof.context -> term -> term - val read_termTs_schematic: Proof.context -> (string -> bool) -> (indexname -> typ option) - -> (indexname -> sort option) -> string list -> (string * typ) list - -> term list * (indexname * typ) list val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term val goal_export: Proof.context -> Proof.context -> thm list -> thm list @@ -118,16 +115,10 @@ (string * typ option * mixfix) list * Proof.context val cert_vars: (string * typ option * mixfix) list -> Proof.context -> (string * typ option * mixfix) list * Proof.context - val read_vars_legacy: (string * string option * mixfix) list -> Proof.context -> - (string * typ option * mixfix) list * Proof.context - val cert_vars_legacy: (string * typ option * mixfix) list -> Proof.context -> - (string * typ option * mixfix) list * Proof.context val add_fixes: (string * string option * mixfix) list -> Proof.context -> string list * Proof.context val add_fixes_i: (string * typ option * mixfix) list -> Proof.context -> string list * Proof.context - val add_fixes_legacy: (string * typ option * mixfix) list -> - Proof.context -> string list * Proof.context val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a) val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context val add_assms: Assumption.export -> @@ -405,8 +396,6 @@ (* type and constant names *) -(* type and constant names *) - fun read_tyname ctxt c = if Syntax.is_tid c then TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (Variable.def_sort ctxt (c, ~1))) @@ -510,29 +499,28 @@ (* decoding raw terms (syntax trees) *) -fun legacy_intern_skolem ctxt internal def_type x = (* FIXME cleanup this mess *) +local + +fun intern_skolem ctxt def_type x = let + val _ = no_skolem false x; val sko = lookup_skolem ctxt x; val is_const = can (read_const_proper ctxt) x; - val is_scoped_const = Variable.is_const ctxt x; - val is_free = (is_some sko orelse not is_const) andalso not is_scoped_const; - val is_internal = internal x; val is_declared = is_some (def_type (x, ~1)); - val res = - if is_free andalso not is_internal then (no_skolem false x; sko) - else ((no_skolem false x; ()) handle ERROR msg => - legacy_feature (msg ^ ContextPosition.str_of ctxt); - if is_internal andalso is_declared then SOME x else NONE); in - if is_some res then res - else if is_declared andalso not is_scoped_const then SOME x else NONE + if Variable.is_const ctxt x then NONE + else if is_some sko then sko + else if not is_const orelse is_declared then SOME x + else NONE end; +in + fun term_context ctxt = let val thy = theory_of ctxt in {get_sort = Sign.get_sort thy (Variable.def_sort ctxt), map_const = try (#1 o Term.dest_Const o read_const_proper ctxt), - map_free = legacy_intern_skolem ctxt (K false) (Variable.def_type ctxt false), + map_free = intern_skolem ctxt (Variable.def_type ctxt false), map_type = Sign.intern_tycons thy, map_sort = Sign.intern_sort thy} end; @@ -541,35 +529,6 @@ let val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt in Syntax.decode_term get_sort map_const map_free map_type map_sort end; - -(* read terms -- legacy *) - -local - -fun read_def_termTs freeze pp syn ctxt (types, sorts, used) fixed sTs = - Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt) fixed - ctxt (types, sorts) used freeze sTs; - -fun append_env e1 e2 x = (case e2 x of NONE => e1 x | some => some); - -fun gen_read' read app schematic ctxt0 internal more_types more_sorts more_used s = - let - val ctxt = if schematic then set_mode mode_schematic ctxt0 else ctxt0; - val types = append_env (Variable.def_type ctxt false) more_types; - val sorts = append_env (Variable.def_sort ctxt) more_sorts; - val used = fold Name.declare more_used (Variable.names_of ctxt); - in - (read (Syntax.pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) - (legacy_intern_skolem ctxt internal types) s - handle TERM (msg, _) => error msg) - |> app (expand_abbrevs ctxt) - |> app (singleton (prepare_patterns ctxt)) - end; - -in - -val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) true; - end; @@ -955,14 +914,12 @@ local -fun prep_vars prep_typ internal legacy = +fun prep_vars prep_typ internal = fold_map (fn (raw_x, raw_T, raw_mx) => fn ctxt => let val (x, mx) = Syntax.const_mixfix raw_x raw_mx; - val _ = - if not legacy andalso not (Syntax.is_identifier (no_skolem internal x)) then - error ("Illegal variable name: " ^ quote x) - else (); + val _ = Syntax.is_identifier (no_skolem internal x) orelse + error ("Illegal variable name: " ^ quote x); fun cond_tvars T = if internal then T @@ -973,10 +930,8 @@ in -val read_vars = prep_vars Syntax.parse_typ false false; -val cert_vars = prep_vars (K I) true false; -val read_vars_legacy = prep_vars Syntax.parse_typ true true; -val cert_vars_legacy = prep_vars (K I) true true; +val read_vars = prep_vars Syntax.parse_typ false; +val cert_vars = prep_vars (K I) true; end; @@ -1079,7 +1034,6 @@ val add_fixes = gen_fixes read_vars; val add_fixes_i = gen_fixes cert_vars; -val add_fixes_legacy = gen_fixes cert_vars_legacy; end;