prep_full_context_statement: explicit record of flags;
authorwenzelm
Mon Mar 30 15:16:58 2009 +0200 (2009-03-30)
changeset 30786461f7b5f16a2
parent 30785 15f64e05e703
child 30794 787b39d499cf
prep_full_context_statement: explicit record of flags;
prep_declaration (for add_locale): disallow autofixed frees;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Mar 30 12:25:52 2009 +1100
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Mar 30 15:16:58 2009 +0200
     1.3 @@ -335,7 +335,7 @@
     1.4  local
     1.5  
     1.6  fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
     1.7 -    strict do_close raw_import init_body raw_elems raw_concl ctxt1 =
     1.8 +    {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
     1.9    let
    1.10      val thy = ProofContext.theory_of ctxt1;
    1.11  
    1.12 @@ -370,6 +370,17 @@
    1.13      val fors = prep_vars_inst fixed ctxt1 |> fst;
    1.14      val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
    1.15      val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
    1.16 +
    1.17 +    val add_free = fold_aterms
    1.18 +      (fn Free (x, T) => not (Variable.is_fixed ctxt3 x) ? insert (op =) (x, T) | _ => I);
    1.19 +    val _ =
    1.20 +      if fixed_frees then ()
    1.21 +      else
    1.22 +        (case fold (fold add_free o snd o snd) insts' [] of
    1.23 +          [] => ()
    1.24 +        | frees => error ("Illegal free variables in expression: " ^
    1.25 +            commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
    1.26 +
    1.27      val ctxt4 = init_body ctxt3;
    1.28      val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
    1.29      val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
    1.30 @@ -410,7 +421,8 @@
    1.31  fun prep_statement prep activate raw_elems raw_concl context =
    1.32    let
    1.33       val ((_, _, elems, concl), _) =
    1.34 -       prep true false ([], []) I raw_elems raw_concl context;
    1.35 +       prep {strict = true, do_close = false, fixed_frees = true}
    1.36 +        ([], []) I raw_elems raw_concl context;
    1.37       val (_, context') = context |>
    1.38         ProofContext.set_stmt true |>
    1.39         fold_map activate elems;
    1.40 @@ -434,7 +446,8 @@
    1.41  fun prep_declaration prep activate raw_import init_body raw_elems context =
    1.42    let
    1.43      val ((fixed, deps, elems, _), (parms, ctxt')) =
    1.44 -      prep false true raw_import init_body raw_elems [] context ;
    1.45 +      prep {strict = false, do_close = true, fixed_frees = false}
    1.46 +        raw_import init_body raw_elems [] context;
    1.47      (* Declare parameters and imported facts *)
    1.48      val context' = context |>
    1.49        fix_params fixed |>
    1.50 @@ -469,7 +482,7 @@
    1.51      val thy = ProofContext.theory_of context;
    1.52  
    1.53      val ((fixed, deps, _, _), _) =
    1.54 -      prep true true expression I [] [] context;
    1.55 +      prep {strict = true, do_close = true, fixed_frees = true} expression I [] [] context;
    1.56      (* proof obligations *)
    1.57      val propss = map (props_of thy) deps;
    1.58