tuned;
authorwenzelm
Thu Oct 11 15:26:33 2012 +0200 (2012-10-11)
changeset 49818db42a1147986
parent 49817 85b37aece3b3
child 49819 97b572c10fe9
tuned;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Oct 11 15:06:27 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Oct 11 15:26:33 2012 +0200
     1.3 @@ -287,13 +287,9 @@
     1.4  
     1.5  (** Finish locale elements **)
     1.6  
     1.7 -fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
     1.8 -      let val x = Binding.name_of binding
     1.9 -      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
    1.10 -  | finish_primitive _ _ (Constrains _) = Constrains []
    1.11 -  | finish_primitive _ close (Assumes asms) = close (Assumes asms)
    1.12 -  | finish_primitive _ close (Defines defs) = close (Defines defs)
    1.13 -  | finish_primitive _ _ (Notes facts) = Notes facts;
    1.14 +fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
    1.15 +  let val x = Binding.name_of binding
    1.16 +  in (binding, AList.lookup (op =) parms x, mx) end);
    1.17  
    1.18  local
    1.19  
    1.20 @@ -320,8 +316,11 @@
    1.21          | e => e)
    1.22        end;
    1.23  
    1.24 -fun finish_elem ctxt parms do_close elem =
    1.25 -  finish_primitive parms (closeup ctxt parms do_close) elem;
    1.26 +fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes)
    1.27 +  | finish_elem _ _ _ (Constrains _) = Constrains []
    1.28 +  | finish_elem ctxt parms do_close (Assumes asms) = closeup ctxt parms do_close (Assumes asms)
    1.29 +  | finish_elem ctxt parms do_close (Defines defs) = closeup ctxt parms do_close (Defines defs)
    1.30 +  | finish_elem _ _ _ (Notes facts) = Notes facts;
    1.31  
    1.32  fun finish_inst ctxt (loc, (prfx, inst)) =
    1.33    let
    1.34 @@ -406,7 +405,7 @@
    1.35      val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
    1.36      val parms = xs ~~ Ts;  (* params from expression and elements *)
    1.37  
    1.38 -    val Fixes fors' = finish_primitive parms I (Fixes fors);
    1.39 +    val fors' = finish_fixes parms fors;
    1.40      val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
    1.41      val (deps, elems'') = finish ctxt6 parms do_close insts elems';
    1.42