src/Pure/Isar/expression.ML
changeset 42494 eef1a23c9077
parent 42482 42c7ef050bc3
child 43543 eb8b4851b039
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Apr 27 20:37:56 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Apr 27 20:58:40 2011 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4      val (implicit, expr') = params_expr expr;
     1.5  
     1.6      val implicit' = map #1 implicit;
     1.7 -    val fixed' = map (Variable.name o #1) fixed;
     1.8 +    val fixed' = map (Variable.check_name o #1) fixed;
     1.9      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
    1.10      val implicit'' =
    1.11        if strict then []
    1.12 @@ -393,7 +393,7 @@
    1.13      val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
    1.14  
    1.15      (* Retrieve parameter types *)
    1.16 -    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes)
    1.17 +    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes)
    1.18        | _ => fn ps => ps) (Fixes fors :: elems') [];
    1.19      val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
    1.20      val parms = xs ~~ Ts;  (* params from expression and elements *)