added add_fixes_direct;
authorwenzelm
Sat Jul 29 00:51:33 2006 +0200 (2006-07-29)
changeset 202516379135f21c2
parent 20250 c3f209752749
child 20252 bad805d0456b
added add_fixes_direct;
tuned;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Sat Jul 29 00:51:32 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Sat Jul 29 00:51:33 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 add_fixes_direct: string list -> Context.proof -> Context.proof
     1.8    val fix_frees: term -> Context.proof -> Context.proof
     1.9    val invent_fixes: string list -> Context.proof -> string list * Context.proof
    1.10    val invent_types: sort list -> Context.proof -> (string * sort) list * Context.proof
    1.11 @@ -235,18 +236,6 @@
    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;
    1.30 @@ -256,6 +245,18 @@
    1.31  
    1.32  end;
    1.33  
    1.34 +
    1.35 +fun add_fixes_direct xs ctxt = ctxt
    1.36 +  |> set_body false
    1.37 +  |> (snd o add_fixes xs)
    1.38 +  |> restore_body ctxt;
    1.39 +
    1.40 +fun fix_frees t ctxt = ctxt
    1.41 +  |> add_fixes_direct
    1.42 +      (rev (fold_aterms (fn Free (x, _) =>
    1.43 +        if is_fixed ctxt x then I else insert (op =) x | _ => I) t []))
    1.44 +  |> declare_term t;
    1.45 +
    1.46  fun invent_types Ss ctxt =
    1.47    let
    1.48      val tfrees = Name.invents (names_of ctxt) "'a" (length Ss) ~~ Ss;