replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
authorwenzelm
Tue Nov 14 22:17:01 2006 +0100 (2006-11-14)
changeset 21370d9dd7b4e5e69
parent 21369 6cca4865e388
child 21371 6717630f080b
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
TFL/rules.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
     1.1 --- a/TFL/rules.ML	Tue Nov 14 22:17:00 2006 +0100
     1.2 +++ b/TFL/rules.ML	Tue Nov 14 22:17:01 2006 +0100
     1.3 @@ -816,7 +816,7 @@
     1.4  fun prove strict (ptm, tac) =
     1.5    let
     1.6      val {thy, t, ...} = Thm.rep_cterm ptm;
     1.7 -    val ctxt = ProofContext.init thy |> Variable.fix_frees t;
     1.8 +    val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
     1.9    in
    1.10      if strict then Goal.prove ctxt [] [] t (K tac)
    1.11      else Goal.prove ctxt [] [] t (K tac)
     2.1 --- a/src/Pure/Isar/locale.ML	Tue Nov 14 22:17:00 2006 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Nov 14 22:17:01 2006 +0100
     2.3 @@ -869,7 +869,7 @@
     2.4          val ts = maps (map #1 o #2) asms';
     2.5          val (ps, qs) = chop (length ts) axs;
     2.6          val (_, ctxt') =
     2.7 -          ctxt |> fold Variable.fix_frees ts
     2.8 +          ctxt |> fold Variable.auto_fixes ts
     2.9            |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
    2.10        in ((ctxt', Assumed qs), []) end
    2.11    | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
    2.12 @@ -881,7 +881,7 @@
    2.13              let val ((c, _), t') = LocalDefs.cert_def ctxt t
    2.14              in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
    2.15          val (_, ctxt') =
    2.16 -          ctxt |> fold (Variable.fix_frees o #1) asms
    2.17 +          ctxt |> fold (Variable.auto_fixes o #1) asms
    2.18            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
    2.19        in ((ctxt', Assumed axs), []) end
    2.20    | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
     3.1 --- a/src/Pure/Isar/proof_context.ML	Tue Nov 14 22:17:00 2006 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Nov 14 22:17:01 2006 +0100
     3.3 @@ -921,8 +921,7 @@
     3.4  (* fixes vs. frees *)
     3.5  
     3.6  fun auto_fixes (arg as (ctxt, (propss, x))) =
     3.7 -  if Variable.is_body ctxt then arg
     3.8 -  else ((fold o fold) Variable.fix_frees propss ctxt, (propss, x));
     3.9 +  ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
    3.10  
    3.11  fun bind_fixes xs ctxt =
    3.12    let
     4.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 14 22:17:00 2006 +0100
     4.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 14 22:17:01 2006 +0100
     4.3 @@ -86,6 +86,7 @@
     4.4  
     4.5  fun read_specification x =
     4.6    prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x;
     4.7 +
     4.8  fun cert_specification x =
     4.9    prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
    4.10  
    4.11 @@ -100,7 +101,7 @@
    4.12  
    4.13      val ((consts, axioms), lthy') = lthy
    4.14        |> LocalTheory.consts spec_frees vars
    4.15 -      ||> fold (fold Variable.fix_frees o snd) specs   (* FIXME !? *)
    4.16 +      ||> fold (fold Variable.auto_fixes o snd) specs   (* FIXME !? *)
    4.17        ||>> LocalTheory.axioms specs;
    4.18  
    4.19      (* FIXME generic target!? *)
    4.20 @@ -206,7 +207,7 @@
    4.21      Element.Shows shows =>
    4.22        let
    4.23          val (_, _, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
    4.24 -        val goal_ctxt = fold (fold (Variable.fix_frees o fst)) propp elems_ctxt;
    4.25 +        val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
    4.26          val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
    4.27        in ((stmt, []), goal_ctxt) end
    4.28    | Element.Obtains obtains =>
    4.29 @@ -232,7 +233,7 @@
    4.30              val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
    4.31            in
    4.32              ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
    4.33 -            ctxt' |> Variable.fix_frees asm
    4.34 +            ctxt' |> Variable.auto_fixes asm
    4.35              |> ProofContext.add_assms_i Assumption.assume_export
    4.36                [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    4.37              |>> (fn [(_, [th])] => th)