src/Pure/Isar/specification.ML
changeset 21370 d9dd7b4e5e69
parent 21359 072e83a0b5bb
child 21435 883337ea2f3b
     1.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 14 22:17:00 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 14 22:17:01 2006 +0100
     1.3 @@ -86,6 +86,7 @@
     1.4  
     1.5  fun read_specification x =
     1.6    prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x;
     1.7 +
     1.8  fun cert_specification x =
     1.9    prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
    1.10  
    1.11 @@ -100,7 +101,7 @@
    1.12  
    1.13      val ((consts, axioms), lthy') = lthy
    1.14        |> LocalTheory.consts spec_frees vars
    1.15 -      ||> fold (fold Variable.fix_frees o snd) specs   (* FIXME !? *)
    1.16 +      ||> fold (fold Variable.auto_fixes o snd) specs   (* FIXME !? *)
    1.17        ||>> LocalTheory.axioms specs;
    1.18  
    1.19      (* FIXME generic target!? *)
    1.20 @@ -206,7 +207,7 @@
    1.21      Element.Shows shows =>
    1.22        let
    1.23          val (_, _, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
    1.24 -        val goal_ctxt = fold (fold (Variable.fix_frees o fst)) propp elems_ctxt;
    1.25 +        val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
    1.26          val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
    1.27        in ((stmt, []), goal_ctxt) end
    1.28    | Element.Obtains obtains =>
    1.29 @@ -232,7 +233,7 @@
    1.30              val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
    1.31            in
    1.32              ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
    1.33 -            ctxt' |> Variable.fix_frees asm
    1.34 +            ctxt' |> Variable.auto_fixes asm
    1.35              |> ProofContext.add_assms_i Assumption.assume_export
    1.36                [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    1.37              |>> (fn [(_, [th])] => th)