tuned;
authorwenzelm
Thu May 12 10:16:52 2016 +0200 (2016-05-12 ago)
changeset 630840054992a86b7
parent 63083 c672c34ab042
child 63085 88474b9fc844
tuned;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu May 12 10:03:17 2016 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu May 12 10:16:52 2016 +0200
     1.3 @@ -250,18 +250,19 @@
     1.4        (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
     1.5    | restore_elem (Notes notes, _) = Notes notes;
     1.6  
     1.7 -fun check cs context =
     1.8 +fun prep (_, pats) (ctxt, t :: ts) =
     1.9 +  let val ctxt' = Variable.auto_fixes t ctxt
    1.10 +  in
    1.11 +    ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
    1.12 +      (ctxt', ts))
    1.13 +  end;
    1.14 +
    1.15 +fun check cs ctxt =
    1.16    let
    1.17 -    fun prep (_, pats) (ctxt, t :: ts) =
    1.18 -      let val ctxt' = Variable.auto_fixes t ctxt
    1.19 -      in
    1.20 -        ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
    1.21 -          (ctxt', ts))
    1.22 -      end;
    1.23 -    val (cs', (context', _)) = fold_map prep cs
    1.24 -      (context, Syntax.check_terms
    1.25 -        (Proof_Context.set_mode Proof_Context.mode_schematic context) (map fst cs));
    1.26 -  in (cs', context') end;
    1.27 +    val (cs', (ctxt', _)) = fold_map prep cs
    1.28 +      (ctxt, Syntax.check_terms
    1.29 +        (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs));
    1.30 +  in (cs', ctxt') end;
    1.31  
    1.32  in
    1.33  
    1.34 @@ -438,15 +439,15 @@
    1.35  
    1.36  local
    1.37  
    1.38 -fun prep_statement prep activate raw_elems raw_stmt context =
    1.39 +fun prep_statement prep activate raw_elems raw_stmt ctxt =
    1.40    let
    1.41      val ((_, _, elems, concl), _) =
    1.42        prep {strict = true, do_close = false, fixed_frees = true}
    1.43 -        ([], []) I raw_elems raw_stmt context;
    1.44 -    val (_, context') = context
    1.45 +        ([], []) I raw_elems raw_stmt ctxt;
    1.46 +    val (_, ctxt') = ctxt
    1.47        |> Proof_Context.set_stmt true
    1.48        |> fold_map activate elems;
    1.49 -  in (concl, context') end;
    1.50 +  in (concl, ctxt') end;
    1.51  
    1.52  in
    1.53  
    1.54 @@ -498,21 +499,21 @@
    1.55      |> map (Morphism.term morph)
    1.56    end;
    1.57  
    1.58 -fun prep_goal_expression prep expression context =
    1.59 +fun prep_goal_expression prep expression ctxt =
    1.60    let
    1.61 -    val thy = Proof_Context.theory_of context;
    1.62 +    val thy = Proof_Context.theory_of ctxt;
    1.63  
    1.64      val ((fixed, deps, _, _), _) =
    1.65        prep {strict = true, do_close = true, fixed_frees = true} expression I []
    1.66 -        (Element.Shows []) context;
    1.67 +        (Element.Shows []) ctxt;
    1.68      (* proof obligations *)
    1.69      val propss = map (props_of thy) deps;
    1.70  
    1.71 -    val goal_ctxt = context |>
    1.72 -      fix_params fixed |>
    1.73 -      (fold o fold) Variable.auto_fixes propss;
    1.74 +    val goal_ctxt = ctxt
    1.75 +      |> fix_params fixed
    1.76 +      |> (fold o fold) Variable.auto_fixes propss;
    1.77  
    1.78 -    val export = Variable.export_morphism goal_ctxt context;
    1.79 +    val export = Variable.export_morphism goal_ctxt ctxt;
    1.80      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
    1.81      val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
    1.82      val exp_typ = Logic.type_map exp_term;