added fix_frees (from Isar/proof_context.ML);
authorwenzelm
Thu Jul 27 23:28:25 2006 +0200 (2006-07-27)
changeset 20240a7b027328d6e
parent 20239 620a3f297072
child 20241 a571d044891e
added fix_frees (from Isar/proof_context.ML);
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Thu Jul 27 23:28:23 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Thu Jul 27 23:28:25 2006 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val thm_context: thm -> Context.proof
     1.5    val variant_frees: Context.proof -> term list -> (string * 'a) list -> (string * 'a) list
     1.6    val add_fixes: string list -> Context.proof -> string list * Context.proof
     1.7 +  val fix_frees: term -> Context.proof -> Context.proof
     1.8    val invent_fixes: string list -> Context.proof -> string list * Context.proof
     1.9    val invent_types: sort list -> Context.proof -> (string * sort) list * Context.proof
    1.10    val export_inst: Context.proof -> Context.proof -> string list * string list
    1.11 @@ -234,6 +235,18 @@
    1.12          (xs, fold Name.declare xs names));
    1.13    in ctxt |> new_fixes names' xs xs' end;
    1.14  
    1.15 +fun fix_frees t ctxt =
    1.16 +  let
    1.17 +    val fixes = rev (fold_aterms (fn Free (x, _) =>
    1.18 +      if is_fixed ctxt x then I else insert (op =) x | _ => I) t []);
    1.19 +  in
    1.20 +    ctxt
    1.21 +    |> set_body false
    1.22 +    |> (snd o add_fixes fixes)
    1.23 +    |> restore_body ctxt
    1.24 +    |> declare_term t
    1.25 +  end;
    1.26 +
    1.27  fun invent_fixes raw_xs ctxt =
    1.28    let
    1.29      val names = names_of ctxt;