renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
authorwenzelm
Sat Mar 28 17:53:33 2009 +0100 (2009-03-28)
changeset 307636976521b4263
parent 30762 cabf9ff3a129
child 30764 3e3e7aa0cc7a
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 17:21:49 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 17:53:33 2009 +0100
     1.3 @@ -181,7 +181,7 @@
     1.4        | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
     1.5      fun mk_avoids params name sets =
     1.6        let
     1.7 -        val (_, ctxt') = ProofContext.add_fixes_i
     1.8 +        val (_, ctxt') = ProofContext.add_fixes
     1.9            (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
    1.10          fun mk s =
    1.11            let
     2.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Sat Mar 28 17:21:49 2009 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sat Mar 28 17:53:33 2009 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4  fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
     2.5      let
     2.6        val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
     2.7 -      val (_, ctx') = ProofContext.add_fixes_i [(Binding.name n', SOME T, NoSyn)] ctx
     2.8 +      val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
     2.9  
    2.10        val (n'', body) = Term.dest_abs (n', T, b) 
    2.11        val _ = (n' = n'') orelse error "dest_all_ctx"
     3.1 --- a/src/Pure/Isar/constdefs.ML	Sat Mar 28 17:21:49 2009 +0100
     3.2 +++ b/src/Pure/Isar/constdefs.ML	Sat Mar 28 17:53:33 2009 +0100
     3.3 @@ -25,13 +25,13 @@
     3.4      fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
     3.5  
     3.6      val thy_ctxt = ProofContext.init thy;
     3.7 -    val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
     3.8 +    val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
     3.9      val ((d, mx), var_ctxt) =
    3.10        (case raw_decl of
    3.11          NONE => ((NONE, NoSyn), struct_ctxt)
    3.12        | SOME raw_var =>
    3.13            struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
    3.14 -            ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
    3.15 +            ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
    3.16  
    3.17      val prop = prep_prop var_ctxt raw_prop;
    3.18      val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
     4.1 --- a/src/Pure/Isar/element.ML	Sat Mar 28 17:21:49 2009 +0100
     4.2 +++ b/src/Pure/Isar/element.ML	Sat Mar 28 17:53:33 2009 +0100
     4.3 @@ -486,7 +486,7 @@
     4.4  local
     4.5  
     4.6  fun activate_elem (Fixes fixes) ctxt =
     4.7 -      ctxt |> ProofContext.add_fixes_i fixes |> snd
     4.8 +      ctxt |> ProofContext.add_fixes fixes |> snd
     4.9    | activate_elem (Constrains _) ctxt =
    4.10        ctxt
    4.11    | activate_elem (Assumes asms) ctxt =
     5.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 28 17:21:49 2009 +0100
     5.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 28 17:53:33 2009 +0100
     5.3 @@ -271,7 +271,7 @@
     5.4  
     5.5  fun declare_elem prep_vars (Fixes fixes) ctxt =
     5.6        let val (vars, _) = prep_vars fixes ctxt
     5.7 -      in ctxt |> ProofContext.add_fixes_i vars |> snd end
     5.8 +      in ctxt |> ProofContext.add_fixes vars |> snd end
     5.9    | declare_elem prep_vars (Constrains csts) ctxt =
    5.10        ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
    5.11    | declare_elem _ (Assumes _) ctxt = ctxt
    5.12 @@ -368,7 +368,7 @@
    5.13        in check_autofix insts elems concl ctxt end;
    5.14  
    5.15      val fors = prep_vars_inst fixed ctxt1 |> fst;
    5.16 -    val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
    5.17 +    val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
    5.18      val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
    5.19      val ctxt4 = init_body ctxt3;
    5.20      val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
    5.21 @@ -426,7 +426,7 @@
    5.22  (* Locale declaration: import + elements *)
    5.23  
    5.24  fun fix_params params =
    5.25 -  ProofContext.add_fixes_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
    5.26 +  ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
    5.27  
    5.28  local
    5.29  
     6.1 --- a/src/Pure/Isar/local_defs.ML	Sat Mar 28 17:21:49 2009 +0100
     6.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Mar 28 17:53:33 2009 +0100
     6.3 @@ -96,7 +96,7 @@
     6.4      val lhss = map (fst o Logic.dest_equals) eqs;
     6.5    in
     6.6      ctxt
     6.7 -    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
     6.8 +    |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
     6.9      |> fold Variable.declare_term eqs
    6.10      |> ProofContext.add_assms_i def_export
    6.11        (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
    6.12 @@ -115,7 +115,7 @@
    6.13      val T = Term.fastype_of rhs;
    6.14      val ([x'], ctxt') = ctxt
    6.15        |> Variable.declare_term rhs
    6.16 -      |> ProofContext.add_fixes_i [(x, SOME T, mx)];
    6.17 +      |> ProofContext.add_fixes [(x, SOME T, mx)];
    6.18      val lhs = Free (x', T);
    6.19      val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
    6.20      fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
     7.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 28 17:21:49 2009 +0100
     7.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 28 17:53:33 2009 +0100
     7.3 @@ -306,7 +306,7 @@
     7.4    in PureThy.note_thmss kind facts' thy |> snd end
     7.5  
     7.6  fun init_local_elem (Fixes fixes) ctxt = ctxt |>
     7.7 -      ProofContext.add_fixes_i fixes |> snd
     7.8 +      ProofContext.add_fixes fixes |> snd
     7.9    | init_local_elem (Assumes assms) ctxt =
    7.10        let
    7.11          val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
     8.1 --- a/src/Pure/Isar/obtain.ML	Sat Mar 28 17:21:49 2009 +0100
     8.2 +++ b/src/Pure/Isar/obtain.ML	Sat Mar 28 17:53:33 2009 +0100
     8.3 @@ -118,7 +118,7 @@
     8.4  
     8.5      (*obtain vars*)
     8.6      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     8.7 -    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
     8.8 +    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
     8.9      val xs = map (Name.of_binding o #1) vars;
    8.10  
    8.11      (*obtain asms*)
     9.1 --- a/src/Pure/Isar/proof.ML	Sat Mar 28 17:21:49 2009 +0100
     9.2 +++ b/src/Pure/Isar/proof.ML	Sat Mar 28 17:53:33 2009 +0100
     9.3 @@ -531,15 +531,15 @@
     9.4  
     9.5  local
     9.6  
     9.7 -fun gen_fix add_fixes args =
     9.8 +fun gen_fix prep_vars args =
     9.9    assert_forward
    9.10 -  #> map_context (snd o add_fixes args)
    9.11 +  #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt))
    9.12    #> put_facts NONE;
    9.13  
    9.14  in
    9.15  
    9.16 -val fix = gen_fix ProofContext.add_fixes;
    9.17 -val fix_i = gen_fix ProofContext.add_fixes_i;
    9.18 +val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
    9.19 +val fix_i = gen_fix (K I);
    9.20  
    9.21  end;
    9.22  
    10.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:21:49 2009 +0100
    10.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:53:33 2009 +0100
    10.3 @@ -108,10 +108,8 @@
    10.4      (binding * typ option * mixfix) list * Proof.context
    10.5    val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
    10.6      (binding * typ option * mixfix) list * Proof.context
    10.7 -  val add_fixes: (binding * string option * mixfix) list ->
    10.8 -    Proof.context -> string list * Proof.context
    10.9 -  val add_fixes_i: (binding * typ option * mixfix) list ->
   10.10 -    Proof.context -> string list * Proof.context
   10.11 +  val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
   10.12 +    string list * Proof.context
   10.13    val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   10.14    val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
   10.15    val add_assms: Assumption.export ->
   10.16 @@ -1105,9 +1103,11 @@
   10.17      error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
   10.18    else (true, (x, T, mx));
   10.19  
   10.20 -fun gen_fixes prep raw_vars ctxt =
   10.21 +in
   10.22 +
   10.23 +fun add_fixes raw_vars ctxt =
   10.24    let
   10.25 -    val (vars, _) = prep raw_vars ctxt;
   10.26 +    val (vars, _) = cert_vars raw_vars ctxt;
   10.27      val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
   10.28      val ctxt'' =
   10.29        ctxt'
   10.30 @@ -1117,11 +1117,6 @@
   10.31        ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   10.32    in (xs', ctxt'') end;
   10.33  
   10.34 -in
   10.35 -
   10.36 -val add_fixes = gen_fixes read_vars;
   10.37 -val add_fixes_i = gen_fixes cert_vars;
   10.38 -
   10.39  end;
   10.40  
   10.41  
   10.42 @@ -1132,7 +1127,7 @@
   10.43  
   10.44  fun bind_fixes xs ctxt =
   10.45    let
   10.46 -    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
   10.47 +    val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
   10.48      fun bind (t as Free (x, T)) =
   10.49            if member (op =) xs x then
   10.50              (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
    11.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Mar 28 17:21:49 2009 +0100
    11.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Mar 28 17:53:33 2009 +0100
    11.3 @@ -283,7 +283,7 @@
    11.4          val (param_names, ctxt') = ctxt
    11.5            |> Variable.declare_thm thm
    11.6            |> Thm.fold_terms Variable.declare_constraints st
    11.7 -          |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
    11.8 +          |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
    11.9  
   11.10          (* Process type insts: Tinsts_env *)
   11.11          fun absent xi = error
    12.1 --- a/src/Pure/Isar/specification.ML	Sat Mar 28 17:21:49 2009 +0100
    12.2 +++ b/src/Pure/Isar/specification.ML	Sat Mar 28 17:53:33 2009 +0100
    12.3 @@ -108,7 +108,7 @@
    12.4      val thy = ProofContext.theory_of ctxt;
    12.5  
    12.6      val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
    12.7 -    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    12.8 +    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
    12.9  
   12.10      val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
   12.11      val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
   12.12 @@ -312,7 +312,7 @@
   12.13                |> fold_map ProofContext.inferred_param xs;
   12.14              val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
   12.15            in
   12.16 -            ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
   12.17 +            ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
   12.18              ctxt' |> Variable.auto_fixes asm
   12.19              |> ProofContext.add_assms_i Assumption.assume_export
   12.20                [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
   12.21 @@ -325,7 +325,7 @@
   12.22          val stmt = [((Binding.empty, atts), [(thesis, [])])];
   12.23  
   12.24          val (facts, goal_ctxt) = elems_ctxt
   12.25 -          |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
   12.26 +          |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
   12.27            |> fold_map assume_case (obtains ~~ propp)
   12.28            |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
   12.29                  [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);