# HG changeset patch # User wenzelm # Date 1238259213 -3600 # Node ID 6976521b4263a029011a8e3e246492c001f04763 # Parent cabf9ff3a129c7e0c57a38d4f6b3dfb737ea1af7 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version; diff -r cabf9ff3a129 -r 6976521b4263 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Mar 28 17:53:33 2009 +0100 @@ -181,7 +181,7 @@ | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)); fun mk_avoids params name sets = let - val (_, ctxt') = ProofContext.add_fixes_i + val (_, ctxt') = ProofContext.add_fixes (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt; fun mk s = let diff -r cabf9ff3a129 -r 6976521b4263 src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Sat Mar 28 17:53:33 2009 +0100 @@ -55,7 +55,7 @@ fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) = let val [(n', _)] = Variable.variant_frees ctx [] [(n,T)] - val (_, ctx') = ProofContext.add_fixes_i [(Binding.name n', SOME T, NoSyn)] ctx + val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx val (n'', body) = Term.dest_abs (n', T, b) val _ = (n' = n'') orelse error "dest_all_ctx" diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/constdefs.ML Sat Mar 28 17:53:33 2009 +0100 @@ -25,13 +25,13 @@ fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); val thy_ctxt = ProofContext.init thy; - val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt); + val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt); val ((d, mx), var_ctxt) = (case raw_decl of NONE => ((NONE, NoSyn), struct_ctxt) | SOME raw_var => struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] => - ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx))); + ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx))); val prop = prep_prop var_ctxt raw_prop; val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop)); diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/element.ML Sat Mar 28 17:53:33 2009 +0100 @@ -486,7 +486,7 @@ local fun activate_elem (Fixes fixes) ctxt = - ctxt |> ProofContext.add_fixes_i fixes |> snd + ctxt |> ProofContext.add_fixes fixes |> snd | activate_elem (Constrains _) ctxt = ctxt | activate_elem (Assumes asms) ctxt = diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/expression.ML Sat Mar 28 17:53:33 2009 +0100 @@ -271,7 +271,7 @@ fun declare_elem prep_vars (Fixes fixes) ctxt = let val (vars, _) = prep_vars fixes ctxt - in ctxt |> ProofContext.add_fixes_i vars |> snd end + in ctxt |> ProofContext.add_fixes vars |> snd end | declare_elem prep_vars (Constrains csts) ctxt = ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd | declare_elem _ (Assumes _) ctxt = ctxt @@ -368,7 +368,7 @@ in check_autofix insts elems concl ctxt end; val fors = prep_vars_inst fixed ctxt1 |> fst; - val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd; + val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd; val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2); val ctxt4 = init_body ctxt3; val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4); @@ -426,7 +426,7 @@ (* Locale declaration: import + elements *) fun fix_params params = - ProofContext.add_fixes_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd; + ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd; local diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/local_defs.ML Sat Mar 28 17:53:33 2009 +0100 @@ -96,7 +96,7 @@ val lhss = map (fst o Logic.dest_equals) eqs; in ctxt - |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2 + |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2 |> fold Variable.declare_term eqs |> ProofContext.add_assms_i def_export (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs) @@ -115,7 +115,7 @@ val T = Term.fastype_of rhs; val ([x'], ctxt') = ctxt |> Variable.declare_term rhs - |> ProofContext.add_fixes_i [(x, SOME T, mx)]; + |> ProofContext.add_fixes [(x, SOME T, mx)]; val lhs = Free (x', T); val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs)); fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]); diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/locale.ML Sat Mar 28 17:53:33 2009 +0100 @@ -306,7 +306,7 @@ in PureThy.note_thmss kind facts' thy |> snd end fun init_local_elem (Fixes fixes) ctxt = ctxt |> - ProofContext.add_fixes_i fixes |> snd + ProofContext.add_fixes fixes |> snd | init_local_elem (Assumes assms) ctxt = let val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/obtain.ML Sat Mar 28 17:53:33 2009 +0100 @@ -118,7 +118,7 @@ (*obtain vars*) val (vars, vars_ctxt) = prep_vars raw_vars ctxt; - val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; + val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars; val xs = map (Name.of_binding o #1) vars; (*obtain asms*) diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/proof.ML Sat Mar 28 17:53:33 2009 +0100 @@ -531,15 +531,15 @@ local -fun gen_fix add_fixes args = +fun gen_fix prep_vars args = assert_forward - #> map_context (snd o add_fixes args) + #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt)) #> put_facts NONE; in -val fix = gen_fix ProofContext.add_fixes; -val fix_i = gen_fix ProofContext.add_fixes_i; +val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt)); +val fix_i = gen_fix (K I); end; diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Mar 28 17:53:33 2009 +0100 @@ -108,10 +108,8 @@ (binding * typ option * mixfix) list * Proof.context val cert_vars: (binding * typ option * mixfix) list -> Proof.context -> (binding * typ option * mixfix) list * Proof.context - val add_fixes: (binding * string option * mixfix) list -> - Proof.context -> string list * Proof.context - val add_fixes_i: (binding * typ option * mixfix) list -> - Proof.context -> string list * Proof.context + val add_fixes: (binding * 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 -> @@ -1105,9 +1103,11 @@ error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x) else (true, (x, T, mx)); -fun gen_fixes prep raw_vars ctxt = +in + +fun add_fixes raw_vars ctxt = let - val (vars, _) = prep raw_vars ctxt; + val (vars, _) = cert_vars raw_vars ctxt; val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt; val ctxt'' = ctxt' @@ -1117,11 +1117,6 @@ ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b)); in (xs', ctxt'') end; -in - -val add_fixes = gen_fixes read_vars; -val add_fixes_i = gen_fixes cert_vars; - end; @@ -1132,7 +1127,7 @@ fun bind_fixes xs ctxt = let - val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs); + val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs); fun bind (t as Free (x, T)) = if member (op =) xs x then (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t) diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/rule_insts.ML --- a/src/Pure/Isar/rule_insts.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/rule_insts.ML Sat Mar 28 17:53:33 2009 +0100 @@ -283,7 +283,7 @@ val (param_names, ctxt') = ctxt |> Variable.declare_thm thm |> Thm.fold_terms Variable.declare_constraints st - |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params); + |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params); (* Process type insts: Tinsts_env *) fun absent xi = error diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Sat Mar 28 17:21:49 2009 +0100 +++ b/src/Pure/Isar/specification.ML Sat Mar 28 17:53:33 2009 +0100 @@ -108,7 +108,7 @@ val thy = ProofContext.theory_of ctxt; val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; - val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; + val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars; val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss; val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss) @@ -312,7 +312,7 @@ |> fold_map ProofContext.inferred_param xs; val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis)); in - ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs)); + ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs)); ctxt' |> Variable.auto_fixes asm |> ProofContext.add_assms_i Assumption.assume_export [((name, [ContextRules.intro_query NONE]), [(asm, [])])] @@ -325,7 +325,7 @@ val stmt = [((Binding.empty, atts), [(thesis, [])])]; val (facts, goal_ctxt) = elems_ctxt - |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]) + |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)]) |> fold_map assume_case (obtains ~~ propp) |-> (fn ths => ProofContext.note_thmss Thm.assumptionK [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);