src/Pure/Isar/expression.ML
changeset 53041 d51bac27d4a0
parent 52732 b4da1f2ec73f
child 54566 5f3e9baa8f13
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Aug 16 19:03:31 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Aug 16 20:58:15 2013 +0200
     1.3 @@ -89,6 +89,8 @@
     1.4  
     1.5  fun parameters_of thy strict (expr, fixed) =
     1.6    let
     1.7 +    val ctxt = Proof_Context.init_global thy;
     1.8 +
     1.9      fun reject_dups message xs =
    1.10        (case duplicates (op =) xs of
    1.11          [] => ()
    1.12 @@ -103,16 +105,18 @@
    1.13              val ps = params_loc loc;
    1.14              val d = length ps - length insts;
    1.15              val insts' =
    1.16 -              if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
    1.17 -                quote (Locale.extern thy loc))
    1.18 +              if d < 0 then
    1.19 +                error ("More arguments than parameters in instantiation of locale " ^
    1.20 +                  quote (Locale.markup_name ctxt loc))
    1.21                else insts @ replicate d NONE;
    1.22              val ps' = (ps ~~ insts') |>
    1.23                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    1.24            in (ps', (loc, (prfx, Positional insts'))) end
    1.25        | params_inst (loc, (prfx, Named insts)) =
    1.26            let
    1.27 -            val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
    1.28 -              (map fst insts);
    1.29 +            val _ =
    1.30 +              reject_dups "Duplicate instantiation of the following parameter(s): "
    1.31 +                (map fst insts);
    1.32              val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
    1.33                if AList.defined (op =) ps p then AList.delete (op =) p ps
    1.34                else error (quote p ^ " not a parameter of instantiated expression"));